### Axiomatics

God created the integers; all else is the work of man. – Leopold Kronecker

The natural numbers have just two building blocks: the initial number
0, and a successor function that gives the next natural number.
*(Back in history, when the natural numbers were first defined, the
number one was treated as the first natural number. Now zero is more
often used. You may say that it’s a modern success story — we start
with nothing and work our way up to everything!)*

We call the natural numbers `NN`

, except sometimes in plain text we
write `\NN`

. `NN x`

means that x is a natural number. For proving
things about the natural numbers you have five fundamental facts in
your toolbox to use at any time:

`NN 0`

`NN x => NN (succ x)`

`NN x => 0 != succ x`

`NN (succ x) & NN (succ y) => x = y`

`P 0 & (P n => P (succ n)) => (NN x => P x)`

These are the standard axioms for the natural numbers, known as the
**Peano axioms** in honor of their discoverer, Giuseppe
Peano.

Stated in English they are that:

- Zero is a natural number.
- The successor of a natural number is also a natural number.
- Zero is the first natural number.
- If two natural numbers have the same successor, then we know they are actually the same.
- (The induction property) Given a property P, if zero has the property, and whenever something has the property its successor also has the property, then all natural numbers have the property.

### Introducing addition

It may seem odd to talk about numbers without the concept of addition. We define addition of natural numbers with two basic facts about addition:

`NN x => x + 0 = x`

— adding zero has no effect`NN x => x + succ y = succ (x + y)`

— adding the next number

Proving some well-known properties of addition from these fundamental
properties will be your challenges, starting with this one, that `NN n => n + succ 0 = succ n`

.

### First addition challenge

*Hint:* start by selecting `n + succ 0`

in the left (assumption) side
of the first step. After that, selecting assumptions (in red) or
parts of assumptions that don’t belong in the result should help you
get good suggestions from the proof builder Basic menu.

My proof of this has five steps: four plus the initial setup.

### Why do some proof steps use `(x = x) == T`

?

You may already be noticing proof steps with descriptions such as “use
`(x = x) == T`

”, or that otherwise contain `== T`

. What are these
about? And why doesn’t Prooftoys just use `x = x`

instead? For
example the fact `NN 0`

is used in this proof to replace `NN 0`

with
T.

The difference is in the policies Prooftoys uses in applying facts for
rewriting. These policies ensure that a request to rewrite a specific
term with a specific fact is never ambiguous. If the fact is either
an equation such as `x = x`

or a conditional equation such as `NN (succ x) & NN (succ y) => x = y`

, rewriting matches the left side of
that equation to do the rewriting.

If the step is neither of these, Prooftoys internally converts it to
an equation. For example it converts `NN x => NN (succ x)`

to `NN x => NN (succ x) == T`

, and `NN 0`

becomes `NN 0 == T`

.

#### ➭ **Next**

**Next**