Axioms for the theory of proveit.numbers.number_sets.natural_numbers

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.

from proveit import m, n, x, S
from proveit.logic import (Boolean, Implies, And, Forall, Equals, NotEquals, 
                           InSet, SetEquiv, SetOfAll, SubsetEq)
from proveit.numbers import zero, one, Add, Natural, NaturalPos, greater

%begin axioms

Defining axioms for theory 'proveit.numbers.number_sets.natural_numbers'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

Peano's axioms define the natural numbers

zero_in_nats = InSet(zero, Natural)

zero_in_nats:

successor_in_nats = Forall(n, InSet(Add(n, one), Natural), domain=Natural)

successor_in_nats:

The following two axioms will ensure that successors are never repeated.

successor_is_injective = Forall((m, n), Equals(n, m), domain=Natural, 
                                condition=Equals(Add(m, one), Add(n, one)))

successor_is_injective:

zero_not_successor = Forall(n, NotEquals(Add(n, one), zero), domain=Natural)

zero_not_successor:

The induction axiom defines the naturals as only zero and its successors and nothing else.

induction = Forall(S, Implies(And(InSet(zero, S), Forall(x, InSet(Add(x, one), S), domain=S)),
                             SetEquiv(S, Natural)),
                   condition=SubsetEq(S, Natural))

induction:

In addition to Peano's axioms, we need an extra axiom to declare that every object is either a Natural or not.

(We must be explicit about defining Natural as a genuine set.)

boolean_natural_membership = Forall(x, InSet(InSet(x, Natural), Boolean))

boolean_natural_membership:

Define the positive naturals (excluding zero)

natural_pos_def = Equals(NaturalPos, SetOfAll(n, n, conditions=[greater(n, zero)], domain=Natural))

natural_pos_def:

%end axioms

These axioms may now be imported from the theory package: proveit.numbers.number_sets.natural_numbers