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

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

In [2]:
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

In [3]:
%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¶

In [4]:
zero_in_nats = InSet(zero, Natural)

zero_in_nats:
In [5]:
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.

In [6]:
successor_is_injective = Forall((m, n), Equals(n, m), domain=Natural,

successor_is_injective:
In [7]:
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.

In [8]:
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.)

In [9]:
boolean_natural_membership = Forall(x, InSet(InSet(x, Natural), Boolean))

boolean_natural_membership:

### Define the positive naturals (excluding zero)¶

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

natural_pos_def:
In [11]:
%end axioms

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