THEOREM
*******
Here, we construct the set of postive rational numbers (qp) using Peano's Axioms, the previously constructed addition (+) and multiplication (*) functions on n, and the Power Set and Subset axioms.
Prove: EXIST(qp):[Set(qp)
& ALL(a):[a e qp
<=> Set'(a)
& ALL(b):ALL(c):[(b,c) e a => b e n & c e n]
&
EXIST(b):EXIST(c):[(b,c)
e
a & ALL(d):ALL(e):[d e
n & e e
n
=> [(d,e)
e
a <=> d*c=e*b]]]]]
This proof was written and verified with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com
PEANO'S AXIOMS
**************
1 Set(n)
Axiom
2 1 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)=1]
Axiom
6 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [1 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Axiom
FROM PREVIOUS RESULTS
*********************
Define: + on n
7 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
8 ALL(a):[a e n => a+1=s(a)]
Axiom
9 ALL(a):ALL(b):[a e n & b e n => a+(b+1)=a+b+1]
Axiom
Define: * on n
10 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
11 ALL(a):[a e n => a*1=a]
Axiom
12 ALL(a):ALL(b):[a e n & b e n => a*(b+1)=a*b+a]
Axiom
13 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
PROOF
*****
Apply Cartesian Product axiom
14
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
15
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, 14
16 Set(n) & Set(n) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
U Spec, 15
17 Set(n) & Set(n)
Join, 1, 1
18 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
Detach, 16, 17
19 Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
E Spec, 18
Define: n2
**********
The set of all ordered pairs of natural numbers
20 Set'(n2)
Split, 19
21 ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
Split, 19
Apply Power Set axiom
22 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
23 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, 22
24 EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e n2]]]
Detach, 23, 20
25 Set(pn2)
& ALL(c):[c e pn2 <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e n2]]
E Spec, 24
Define: pn2
***********
The power set of n2
26 Set(pn2)
Split, 25
27 ALL(c):[c e pn2 <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e n2]]
Split, 25
28
EXIST(sub):[Set(sub)
& ALL(a):[a e
sub <=> a
e pn2
& EXIST(b):EXIST(c):[(b,c)
e a
& ALL(d):ALL(e):[d
e n
& e e
n
=> [(d,e) e
a <=> b*e=d*c]]]]]
Subset, 26
29
Set(qp)
& ALL(a):[a e
qp
<=> a e
pn2
& EXIST(b):EXIST(c):[(b,c)
e a
& ALL(d):ALL(e):[d
e n
& e e
n
=> [(d,e) e
a <=> b*e=d*c]]]]
E Spec, 28
Define: qp
**********
The set of positive rational numbers
30 Set(qp)
Split, 29
31
ALL(a):[a
e qp
<=> a e
pn2
& EXIST(b):EXIST(c):[(b,c)
e a &
ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e)
e a <=> b*e=d*c]]]]
Split, 29
Recast this definition without reference to pn2
'=>'
Prove: ALL(a):[a e qp
=> Set'(a)
& ALL(b):ALL(c):[(b,c) e a => b e n & c e n]
&
EXIST(b):EXIST(c):[(b,c)
e
a & ALL(d):ALL(e):[d e
n & e e
n
=> [(d,e)
e
a <=> b*e=d*c]]]]
Suppose...
32 x e qp
Premise
Apply definition of qp
33
x
e qp
<=> x
e pn2
& EXIST(b):EXIST(c):[(b,c)
e x
& ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e)
e x
<=> b*e=d*c]]]
U Spec, 31
34
[x
e qp
=> x
e pn2
& EXIST(b):EXIST(c):[(b,c)
e x
& ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e)
e x
<=> b*e=d*c]]]]
& [x
e pn2
& EXIST(b):EXIST(c):[(b,c)
e x
& ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e)
e x
<=> b*e=d*c]]] =>
x e
qp]
Iff-And, 33
35
x
e qp
=> x
e pn2
& EXIST(b):EXIST(c):[(b,c)
e x
& ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e)
e x
<=> b*e=d*c]]]
Split, 34
36
x
e pn2
& EXIST(b):EXIST(c):[(b,c)
e x
& ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e)
e x
<=> b*e=d*c]]] =>
x e
qp
Split, 34
37
x
e pn2
& EXIST(b):EXIST(c):[(b,c)
e x
& ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e)
e x
<=> b*e=d*c]]]
Detach, 35, 32
38 x e pn2
Split, 37
39 EXIST(b):EXIST(c):[(b,c) e x & ALL(d):ALL(e):[d e n & e e n => [(d,e) e x <=> b*e=d*c]]]
Split, 37
Apply definition of pn2
40 x e pn2 <=> Set'(x) & ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2]
U Spec, 27
41 [x e pn2 => Set'(x) & ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2]]
& [Set'(x) & ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2] => x e pn2]
Iff-And, 40
42 x e pn2 => Set'(x) & ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2]
Split, 41
43 Set'(x) & ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2] => x e pn2
Split, 41
44 Set'(x) & ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2]
Detach, 42, 38
45 Set'(x)
Split, 44
46 ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2]
Split, 44
Prove: ALL(b):ALL(c):[(b,c) e x => b e n & c e n]
Suppose...
47 (t,u) e x
Premise
48 ALL(d2):[(t,d2) e x => (t,d2) e n2]
U Spec, 46
49 (t,u) e x => (t,u) e n2
U Spec, 48
50 (t,u) e n2
Detach, 49, 47
Apply definition of n2
51 ALL(c2):[(t,c2) e n2 <=> t e n & c2 e n]
U Spec, 21
52 (t,u) e n2 <=> t e n & u e n
U Spec, 51
53 [(t,u) e n2 => t e n & u e n]
& [t e n & u e n => (t,u) e n2]
Iff-And, 52
54 (t,u) e n2 => t e n & u e n
Split, 53
55 t e n & u e n => (t,u) e n2
Split, 53
56 t e n & u e n
Detach, 54, 50
As Required:
57 ALL(b):ALL(c):[(b,c) e x => b e n & c e n]
4 Conclusion, 47
Joining results...
58 Set'(x)
& ALL(b):ALL(c):[(b,c) e x => b e n & c e n]
Join, 45, 57
59 Set'(x)
& ALL(b):ALL(c):[(b,c) e x => b e n & c e n]
& EXIST(b):EXIST(c):[(b,c) e x & ALL(d):ALL(e):[d e n & e e n => [(d,e) e x <=> b*e=d*c]]]
Join, 58, 39
As Required:
60 ALL(a):[a e qp
=> Set'(a)
& ALL(b):ALL(c):[(b,c) e a => b e n & c e n]
& EXIST(b):EXIST(c):[(b,c) e a & ALL(d):ALL(e):[d e n & e e n => [(d,e) e a <=> b*e=d*c]]]]
4 Conclusion, 32
'<='
Prove: ALL(a):[Set'(a)
& ALL(b):ALL(c):[(b,c) e a => b e n & c e n]
&
EXIST(b):EXIST(c):[(b,c)
e
a & ALL(d):ALL(e):[d e
n & e e
n
=> [(d,e)
e
a <=> b*e=d*c]]]
=> a e qp]
Suppose...
61 Set'(x)
& ALL(b):ALL(c):[(b,c) e x => b e n & c e n]
& EXIST(b):EXIST(c):[(b,c) e x & ALL(d):ALL(e):[d e n & e e n => [(d,e) e x <=> b*e=d*c]]]
Premise
62 Set'(x)
Split, 61
63 ALL(b):ALL(c):[(b,c) e x => b e n & c e n]
Split, 61
64 EXIST(b):EXIST(c):[(b,c) e x & ALL(d):ALL(e):[d e n & e e n => [(d,e) e x <=> b*e=d*c]]]
Split, 61
Apply definition of qp
65
x
e qp
<=> x
e pn2
& EXIST(b):EXIST(c):[(b,c)
e x
& ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e)
e x
<=> b*e=d*c]]]
U Spec, 31
66
[x
e qp
=> x
e pn2
& EXIST(b):EXIST(c):[(b,c)
e x
& ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e)
e x
<=> b*e=d*c]]]]
& [x
e pn2
& EXIST(b):EXIST(c):[(b,c)
e x
& ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e)
e x
<=> b*e=d*c]]] =>
x
e qp]
Iff-And, 65
67
x
e qp
=> x
e pn2
& EXIST(b):EXIST(c):[(b,c)
e x
& ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e)
e x
<=> b*e=d*c]]]
Split, 66
Sufficient For: x e qp
68
x
e pn2
& EXIST(b):EXIST(c):[(b,c)
e x
& ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e)
e x
<=> b*e=d*c]]] =>
x
e qp
Split, 66
Apply definition of pn2
69 x e pn2 <=> Set'(x) & ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2]
U Spec, 27
70 [x e pn2 => Set'(x) & ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2]]
& [Set'(x) & ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2] => x e pn2]
Iff-And, 69
71 x e pn2 => Set'(x) & ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2]
Split, 70
Sufficient For: x e pn2
72 Set'(x) & ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2] => x e pn2
Split, 70
Prove: ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2]
Suppose...
73 (t,u) e x
Premise
Apply definition of x
74 ALL(c):[(t,c) e x => t e n & c e n]
U Spec, 63
75 (t,u) e x => t e n & u e n
U Spec, 74
76 t e n & u e n
Detach, 75, 73
Apply definition for n2
77 ALL(c2):[(t,c2) e n2 <=> t e n & c2 e n]
U Spec, 21
78 (t,u) e n2 <=> t e n & u e n
U Spec, 77
79 [(t,u) e n2 => t e n & u e n]
& [t e n & u e n => (t,u) e n2]
Iff-And, 78
80 (t,u) e n2 => t e n & u e n
Split, 79
81 t e n & u e n => (t,u) e n2
Split, 79
82 (t,u) e n2
Detach, 81, 76
As Required:
83 ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2]
4 Conclusion, 73
84 Set'(x)
& ALL(d1):ALL(d2):[(d1,d2) e x => (d1,d2) e n2]
Join, 62, 83
85 x e pn2
Detach, 72, 84
86 x e pn2
& EXIST(b):EXIST(c):[(b,c) e x & ALL(d):ALL(e):[d e n & e e n => [(d,e) e x <=> b*e=d*c]]]
Join, 85, 64
87 x e qp
Detach, 68, 86
As Required:
88 ALL(a):[Set'(a)
& ALL(b):ALL(c):[(b,c) e a => b e n & c e n]
& EXIST(b):EXIST(c):[(b,c) e a & ALL(d):ALL(e):[d e n & e e n => [(d,e) e a <=> b*e=d*c]]]
=> a e qp]
4 Conclusion, 61
Joining results...
89 ALL(a):[[a e qp
=> Set'(a)
& ALL(b):ALL(c):[(b,c) e a => b e n & c e n]
&
EXIST(b):EXIST(c):[(b,c)
e a &
ALL(d):ALL(e):[d e
n
& e e
n
=> [(d,e) e
a <=> b*e=d*c]]]]
& [Set'(a)
& ALL(b):ALL(c):[(b,c) e a => b e n & c e n]
& EXIST(b):EXIST(c):[(b,c) e a & ALL(d):ALL(e):[d e n & e e n => [(d,e) e a <=> b*e=d*c]]]
=> a e qp]]
Join, 60, 88
As Required:
90 ALL(a):[a e qp
<=> Set'(a)
& ALL(b):ALL(c):[(b,c) e a => b e n & c e n]
& EXIST(b):EXIST(c):[(b,c) e a & ALL(d):ALL(e):[d e n & e e n => [(d,e) e a <=> b*e=d*c]]]]
Iff-And, 89
As Required:
91 EXIST(qp):ALL(a):[a e qp
<=> Set'(a)
& ALL(b):ALL(c):[(b,c) e a => b e n & c e n]
& EXIST(b):EXIST(c):[(b,c) e a & ALL(d):ALL(e):[d e n & e e n => [(d,e) e a <=> b*e=d*c]]]]
E Gen, 90