Go up to 4 NumbersGo forward to 4.2 The Integer Numbers |

**Peano Arithmetic**
We may consider the natural numbers as an elementary domain by a
*theory* that is due to the mathematician Peano.

- 0 is not the successor of any natural number:
**forall**`x`:`x`' != 0. - Different natural numbers have different successors:
**forall**`x`,`y`:`x`' =`y`' =>`x`=`y`. - For every formula
`F`, we have an axiom that states:`F`holds for every natural number, if`F`holds for 0 and with every number also for its successor, i.e.,(

We call these axioms the`F`[`x`<- 0] /\ (**forall**`x`:`F`=>`F`[`x`<-`x`+1])) =>**forall**`x`:`F`.*induction axioms (Induktionsaxiome)*.

The Peano axioms essentially state that the natural numbers are a single infinite chain

0 -> 0' -> 0" -> 0"' -> ...We will see later how all operations on the natural numbers can be defined just on the basis of 0 and '.

**Construction from Sets**
It is not necessary to consider the natural numbers as elementary objects;
they can be *defined* within the framework of set theory that provides a
more fundamental kind of objects.

0 := 0;x' :=xunion {x}.

The first two axioms of Peano arithmetic are consequences of this definition.

- We prove
**forall**`x`:`x`' != 0. Take arbitrary`x`. By definition of 0 and ', we have to prove`x`union {`x`} !=**0**`x`in (`x`union {`x`}) but`x`!=**0**. - We prove
**forall**`x`,`y`:`x`' =`y`' =>`x`=`y`. Take arbitrary`x`and`y`. We assume(1)

and have to show`x`' =`y`'`x`=`y`. We assume (2)`x`!=`y`and show a contradiction. From (1), we know by the definition of '(3)

By the definition of union and set enumeration, we know (4)`x`union {`x`} =`y`union {`y`}.`x`in`x`union {`x`} and (5)`y`in`y`union {`y`}. From (3), (4), and the definition of =, we have (6)`x`in`y`union {`y`} which implies with (2)(7)

Likewise, we have from (3), (5), and the definition of = that (8)`x`in`y`.`y`in`x`union {`x`} which implies with (2)(9)

The conjunction of (7) and (9) is in contradiction to the set-theoretic axiom of`y`in`x`.*regularity (Regularität)*that prohibits such "cycles" (in general any infinitely descending chains) with respect to in .

The construction of natural numbers proceeds with the definition of a set **N**
(which we do not give) such that the following proposition holds.

0 in N;forallxinN:x' inN;for every formula F:( F(0) /\forallxinN:F(x) =>F(x+1)) =>forallxinN:F(x).

Thus also the third law of Peano holds in the set-based construction of natural numbers. Sometimes the following notations will be used.

N_{>0}:= { xinN:x> 0};N_{n}:= { xinN:x<n}.

**Arithmetic Operations** Independently of how we have
introduced the natural numbers, we can define the basic arithmetic operations
with the help of the functions 0 and ' and the following auxiliary
operation.

x^{-}:=suchy:x=y'.

Because of the second Peano law, the predecessor is uniquely defined (if it
exists). However, because of the first Peano law, there is no `x` such
that `x`' = 0 and thus 0^{-} is undefined (and we must not assume
0^{-}' = 0).

We now introduce the arithmetic operations by *recursive
definitions*. In the rest of this section, all variables denote
natural numbers.

**Constants**1 := 0', 2 := 1'; **Addition**`x`+`y`:=**if**`y`= 0**then**`x`**else**(`x`+`y`^{-})'**Multiplication**`x`*`y`:=**if**`y`= 0**then**0**else**`x`+(`x`*`y`^{-})**Total Order**`x`<=`y`: <=>**if**`x`= 0**then**T**else if**`y`= 0**then**F**else**`x`^{-}<=`y`^{-}

The recursive definitions are constructive in the sense that they can be executed by repeated "unfolding" of the definition.

1+2 = (definitions of 1 and 2) 0' + 0" = = (definition of +) ( if0" = 0then0'else(0'+0"^{-})')= (second Peano law) (0'+0" ^{-})'= (definition of ^{-})(0'+0')' = (definition of +) ( if0' = 0then0'else(0'+0'^{-})')'= (second Peano law) (0'+0' ^{-})"= (definition of ^{-})(0'+0)" = (definition of +) ( if0 = 0then0'else(0'+0^{-})')"= (reflexivity of =) 0"'.

**Natural Number Laws**
Immediate consequences of these definitions are the following laws.

**Addition**`x`+ 0= `x`,`x`+`y`'= ( `x`+`y`)';**Multiplication**`x`* 0= 0, `x`*`y`'= x+( `x`*`y`);**Total Order**`0`<=`x`<=> T, `x`<= 0<=> `x`= 0,`x`' <=`y`'<=> `x`<=`y`.

Furthermore, the following well known laws hold.

x+ 0= x,x* 1= x,x+y= y+x,x*y= y*x,x+ (y+z)= ( x+y) +z,x* (y*z)= ( x*y) *z,x* (y+z)= ( x*y) + (x*z),x<= x,( x<=y/\y<=x)=> x=y,( x<=y/\y<=z)=> x<=z.

We will use the following abbreviations for every domain that provides a binary predicate <= .

x<y: <=>x<=y/\x!=y;x>y: <=>xnot <=y;x>=y: <=>xnot <y.

We often write `a` <= `x` < `b` to denote `x` <= `a` /\ `x` < `b` and similar for all other combinations of
the order predicates.

**Logic Evaluator** Although there is a builtin implementation of the
natural numbers, we are going to simulate the construction on the base of 0
and and '; we use the letter `N`

to distinguish the natural number
function and predicate constants from those that are going to be introduced in
the following sections. These and the subsequent definitions are collected in
Appendix * natural.txt*.

**More Operations**
Since we have addition, we would also like to have the inverse operation.

x-y:=suchz:x=z+y.

Please note that a difference between two natural numbers does not always
exist, e.g. 1-2 is undefined because there is no `z` with
`1`=`z`+`2` (and we must not assume 1 = (1-2)+2).
However, we have the following result.

Ifforallx,y,z_{0},z_{1}: (x=z_{0}+y/\x=z_{1}+y) =>z_{0}=z_{1}.

forallx,y:x>=y=>x= (x-y)+y.

At the moment, we state these propositions without proofs. In
Chapter *Induction*, we will discuss in detail how to prove
properties about natural numbers.

While the natural numbers do not have an operation for exact division, they provide the following pair of functions.

xdivy:= suchq:existsr:r<y/\x=(q*y)+r;xmody:= suchr:existsq:r<y/\x=(q*y)+r.

By above definition (`x` div 0) and (`x` mod
0) are undefined for every `x`. On the other side, we have the
following positive results.

If the divisor is not null, quotient and remainder exist:

forallx,y,q_{0},q_{1},r_{0}<y,r_{1}<y:( x=(q_{0}*y)+r_{0}/\x=(q_{1}*y)+r_{1}) => (q_{0}=q_{1}/\r_{0}=r_{1}).

We thus have the following relationship between quotient and remainder:

forallx,y!= 0: (existsq,r:r<y/\x= (q*y)+r).

forallx,y!= 0:x= (xdivy)*y+ (xmody).

We define exponentiation as shown below.

. ^{.}:NxN->N,x^{n}:=ifn= 0then1elsex*x^{n-}.

A corresponding construction can be applied in every domain `D` with a
constant 1 and a binary function * such as the number domains that will be
introduced in the following sections; we will then assume the existence of a
corresponding function .^{.}: `D` x **N** -> `D`.

**Logic Evaluator** Difference, quotient, remainder and
exponentiation are defined as shown below.

Other important notions on natural numbers can be introduced as follows.

`x`*divides*`y`if`x`*`z`=`y`for some`z`:`x`|`y`: <=>**exists**`z`:`x`*`z`=`y`.- The
*greatest common divisor (größter gemeinsamer Teiler)*of`x`and`y`is the largest number that divides both`x`and`y`:gcd(

`x`,`y`) :=**such**z:`z`|`x`/\`z`|`y`/\ (**forall**w: (`w`|`x`/\`w`|`y`) =>`w`<=`z`). - The
*least common multiple (kleinstes gemeinsames Vielfaches)*of`x`and`y`is the smallest number that both`x`and`y`divide:lcm(

`x`,`y`) :=**such**z:`x`|`z`/\`y`|`z`/\ (**forall**w: (`x`|`w`/\`y`|`w`) =>`z`<=`w`). - Two numbers are
*relatively prime (relativ prim)*if their greatest common divisor is 1:`x`and`y`are relatively prime : <=> gcd(`x`,`y`) = 1. - A number greater than 1 is
*prime (prim)*if its only divisors are are 1 and itself:`x`is prime : <=>`x`> 1 /\ (**forall**y:`y`|`x`=> (`y`= 1 \/`y`=`x`)).

The definition of prime numbers is motivated by the fact that every positive
natural number `n` has a unique prime number factorization (which will be
stated formally in Proposition *Prime Number
Factorization*).

**Logic Evaluator** Above notions are defined as shown below
(to speed up computation, we we revert to builtin natural number arithmetic
using the file `natural0.txt`

.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999