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)
In [5]:
successor_in_nats = Forall(n, InSet(Add(n, one), Natural), domain=Natural)

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)))
In [7]:
zero_not_successor = Forall(n, NotEquals(Add(n, one), zero), domain=Natural)

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

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

Define the positive naturals (excluding zero)

In [10]:
natural_pos_def = Equals(NaturalPos, SetOfAll(n, n, conditions=[greater(n, zero)], domain=Natural))
In [11]:
%end axioms
These axioms may now be imported from the theory package: proveit.numbers.number_sets.natural_numbers