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
```

In [4]:

```
zero_in_nats = InSet(zero, Natural)
```

Out[4]:

In [5]:

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

Out[5]:

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

In [6]:

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

Out[6]:

In [7]:

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

Out[7]:

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))
```

Out[8]:

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

In [9]:

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

Out[9]:

In [10]:

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

Out[10]:

In [11]:

```
%end axioms
```