Constructing the set of
integers from Peano’s Axioms
****************************************************
By Dan Christensen
2024-11-21
Informally, we have:
+-0 :=
{(0, 0), (1, 1), (2, 2), ... }
+1 := {(1, 0), (2, 1), (3, 2), ... }
-1 := {(0, 1), (1, 2), (2, 3), ... }
+2 := {(2, 0), (3, 1), (4, 2), ... }
-2 := {(0, 2), (1, 3), (2, 4), ... }
Peano's Axioms
**************
1 Set(n)
Axiom
2 0 e n
Axiom
3 ALL(a):[a e n => s(a) e n]
Axiom
4 ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
Axiom
5 ALL(a):[a e n => ~s(a)=0]
Axiom
6 ALL(a):[Set(a) &
ALL(b):[b e a => b e n]
=>
[0 e a & ALL(b):[b e a => s(b) e a]
=>
ALL(b):[b e n => b e a]]]
Axiom
Introducing + function
**********************
7 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
8 ALL(a):[a e n => s(a)=a+1]
Axiom
Proof
*****
Construct n2 (set of ordered pairs n x n)
9 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
10 ALL(a2):[Set(n) & Set(a2)
=> EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e a2]]]
U Spec, 9
11 Set(n) & Set(n) =>
EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
U Spec, 10
12 Set(n) & Set(n)
Join, 1, 1
13 EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
Detach, 11, 12
14 Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
E Spec, 13
15 Set'(n2)
Split, 14
16 ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
Split, 14
Construct pn2 (power set of n2)
17 ALL(a):[Set'(a) => EXIST(b):[Set(b)
&
ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e a]]]]
Power Set
18 Set'(n2) => EXIST(b):[Set(b)
&
ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e n2]]]
U Spec, 17
19 EXIST(b):[Set(b)
&
ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e n2]]]
Detach, 18, 15
20 Set(pn2)
&
ALL(c):[c e pn2 <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e n2]]
E Spec, 19
21 Set(pn2)
Split, 20
22 ALL(c):[c e pn2 <=> Set'(c) &
ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e n2]]
Split, 20
Construct nneg (non-negative integers)
23 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e pn2 & EXIST(b):[b e n &
ALL(c):ALL(d):[(c,d) e a => c=d+b]]]]
Subset, 21
24 Set(nneg) & ALL(a):[a e nneg <=> a e pn2 &
EXIST(b):[b e n & ALL(c):ALL(d):[(c,d) e a => c=d+b]]]
E Spec, 23
25 Set(nneg)
Split, 24
26 ALL(a):[a e nneg <=> a e pn2 & EXIST(b):[b e n &
ALL(c):ALL(d):[(c,d) e a => c=d+b]]]
Split, 24
Construct npos (non-positive integers)
27 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e pn2 & EXIST(b):[b e n &
ALL(c):ALL(d):[(c,d) e a => d=c+b]]]]
Subset, 21
28 Set(npos) & ALL(a):[a e npos <=> a e pn2 &
EXIST(b):[b e n & ALL(c):ALL(d):[(c,d) e a => d=c+b]]]
E Spec, 27
29 Set(npos)
Split, 28
30 ALL(a):[a e npos <=> a e pn2 & EXIST(b):[b e n &
ALL(c):ALL(d):[(c,d) e a => d=c+b]]]
Split, 28
Construct int
(set of integers)
Applying pairwise union
31 ALL(a):ALL(b):[Set(a)
& Set(b) => EXIST(c):[Set(c) & ALL(d):[d e c <=> d e a | d e b]]]
Pw Union
32 ALL(b):[Set(nneg) & Set(b) => EXIST(c):[Set(c) &
ALL(d):[d e c <=> d e nneg | d e b]]]
U Spec, 31
33 Set(nneg) & Set(npos) =>
EXIST(c):[Set(c) & ALL(d):[d e c <=> d e nneg | d e npos]]
U Spec, 32
34 Set(nneg) & Set(npos)
Join, 25, 29
35 EXIST(c):[Set(c) & ALL(d):[d e c <=> d e nneg | d e npos]]
Detach, 33, 34
Define: int
(set of integers, pairwise union of nneg
and npos)
36 Set(int) &
ALL(d):[d e int <=> d e nneg | d e npos]
E Spec, 35