In [1]:

```
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit.logic import And, Equals, Forall, Iff, Implies, InSet, SetEquiv, SetOfAll, SubsetProper, Union
from proveit.numbers import Complex, Integer, Interval, Natural, NaturalPos, Neg
from proveit.numbers import Add, greater, Less, LessEq, number_ordering
from proveit.numbers import zero, one, num
from proveit import a, b, n, m, x, y, S
%begin axioms
```

**Define the set of naturals, $\mathbb{N}$, as, essentially, the minimal set that contains zero and all of its successors:**

In [2]:

```
#naturals_def = Forall(n, Equals(InSet(n, Natural), Forall(S, Implies(And(InSet(zero, S), Forall(x, InSet(Add(x,one), S), domain=S)), InSet(n, S)))))
```

that is, $n \in \mathbb{N}$ iff n is in all sets that contain zero and all successors.

**Define the integers, $\mathbb{Z}$ as the union of the naturals and the negated positive naturals (i.e., the positive and negative forms of all natural numbers where zero is its own negative):**

In [3]:

```
integers_def = Equals(Integer, Union(Natural, SetOfAll(n, Neg(n), domain=NaturalPos)))
```

**Defining properties of individual natural numbers:**

In [4]:

```
#add_by_zero = Forall(x, Equals(Add(x, zero), x), domain=Complex)
```

In [5]:

```
integer_interval_is_subset_of_integers = Forall(
(a, b),
SubsetProper(Interval(a, b), Integer),
domain = Integer)
```

Note: if $b < a$, $\{a~\ldotp \ldotp~b\}$ is equivalent to the empty set.

In [6]:

```
integer_interval_element_bounds = Forall(
(a, b),
Forall(n,
number_ordering(LessEq(a, n), LessEq(n, b)),
domain = Interval(a, b)),
domain = Integer)
```

In [7]:

```
# Consider this as an alternative??
# from proveit import ExprRange
# from proveit.logic import Set
#Forall((a, b), Equals(Interval(a, b), Set(ExprRange(n, n, a, b))), domain=Integer)
```

In [8]:

```
%end axioms
```