Construct the Positive Real Numbers

THEOREM

*******

We can construct, i.e. prove the existence of the set of positive real numbers (rp) starting from Peano's Axioms.

Prove: EXIST(rp):ALL(a):[a e rp

<=> Set(a) & ALL(d):[d e a => d e qp]

& EXIST(b):b e a

& EXIST(b):[b e qp & ~b e a]

& ALL(b):[b e a => ALL(c):[c e qp => [c c e a]]]

& ALL(b):[b e a => EXIST(c):[c e a & b<c]]]

where < is the ordering on the set of positive rational numbers qp.

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: qp

**********

The set of positive rational numbers where < is the ordering on the set of natural numbers

7 Set(qp)

Axiom

8 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]]]]

Axiom

Define: < on qp

***************

Note that the '<' to the right of the biconditional refers to the ordering on the set of natural numbers.

The variables c, d, e, f will always be natural numbers.

9 ALL(a):ALL(b):[a e qp & b e qp

=> [a<b

<=> ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e a & (e,f) e b => c*f<e*d]]]

Axiom

Define: < on n

**************

10 ALL(a):ALL(b):[a e n & b e n => [a EXIST(c):[c e n & a+c=b]]]

Axiom

Define: + on n

**************

11 ALL(a):ALL(b):[a e n & b e n => a+b e n]

& ALL(a):[a e n => a+1=s(a)]

& ALL(a):ALL(b):[a e n & b e n => a+s(b)=s(a+b)]

Axiom

Define: * on n

**************

12 ALL(a):ALL(b):[a e n & b e n => a*b e n]

& ALL(a):[a e n => a*1=a]

& ALL(a):ALL(b):[a e n & b e n => a*(b+1)=a*b+a]

Axiom

PROOF

*****

Apply the Power Set Axiom

13 ALL(a):[Set(a) => EXIST(b):[Set(b)

& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e a]]]]

Power Set

14 Set(qp) => EXIST(b):[Set(b)

& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e qp]]]

U Spec, 13

15 EXIST(b):[Set(b)

& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e qp]]]

Detach, 14, 7

16 Set(pqp)

& ALL(c):[c e pqp <=> Set(c) & ALL(d):[d e c => d e qp]]

E Spec, 15

Define: pqp

***********

The power set of qp

17 Set(pqp)

Split, 16

18 ALL(c):[c e pqp <=> Set(c) & ALL(d):[d e c => d e qp]]

Split, 16

Apply the Subset Axiom

19 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e pqp & [EXIST(b):b e a

& EXIST(b):[b e qp & ~b e a]

& ALL(b):[b e a => ALL(c):[c e qp => [c c e a]]]

& ALL(b):[b e a => EXIST(c):[c e a & b<c]]]]]

Subset, 17

20 Set(rp) & ALL(a):[a e rp <=> a e pqp & [EXIST(b):b e a

& EXIST(b):[b e qp & ~b e a]

& ALL(b):[b e a => ALL(c):[c e qp => [c c e a]]]

& ALL(b):[b e a => EXIST(c):[c e a & b<c]]]]

E Spec, 19

Define: rp

The set of positive real numbers

21 Set(rp)

Split, 20

22 ALL(a):[a e rp <=> a e pqp & [EXIST(b):b e a

& EXIST(b):[b e qp & ~b e a]

& ALL(b):[b e a => ALL(c):[c e qp => [c c e a]]]

& ALL(b):[b e a => EXIST(c):[c e a & b<c]]]]

Split, 20

Recast this definition without making reference to the set pqp.

'=>'

Prove: ALL(a):[a e rp

=> Set(a) & ALL(d):[d e a => d e qp]

& EXIST(b):b e a

& EXIST(b):[b e qp & ~b e a]

& ALL(b):[b e a => ALL(c):[c e qp => [c c e a]]]

& ALL(b):[b e a => EXIST(c):[c e a & b<c]]]

Suppose...

23 x e rp

Premise

Apply definition of rp

24 x e rp <=> x e pqp & [EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]]

U Spec, 22

25 [x e rp => x e pqp & [EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]]]

& [x e pqp & [EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]] => x e rp]

Iff-And, 24

26 x e rp => x e pqp & [EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]]

Split, 25

27 x e pqp & [EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]] => x e rp

Split, 25

28 x e pqp & [EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]]

Detach, 26, 23

29 x e pqp

Split, 28

30 EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]

Split, 28

31 EXIST(b):b e x

Split, 30

32 EXIST(b):[b e qp & ~b e x]

Split, 30

33 ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

Split, 30

34 ALL(b):[b e x => EXIST(c):[c e x & b<c]]

Split, 30

Apply definition of pqp

35 x e pqp <=> Set(x) & ALL(d):[d e x => d e qp]

U Spec, 18

36 [x e pqp => Set(x) & ALL(d):[d e x => d e qp]]

& [Set(x) & ALL(d):[d e x => d e qp] => x e pqp]

Iff-And, 35

37 x e pqp => Set(x) & ALL(d):[d e x => d e qp]

Split, 36

38 Set(x) & ALL(d):[d e x => d e qp] => x e pqp

Split, 36

39 Set(x) & ALL(d):[d e x => d e qp]

Detach, 37, 29

Joining results...

40 Set(x) & ALL(d):[d e x => d e qp]

& EXIST(b):b e x

Join, 39, 31

41 Set(x) & ALL(d):[d e x => d e qp]

& EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

Join, 40, 32

42 Set(x) & ALL(d):[d e x => d e qp]

& EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

Join, 41, 33

43 Set(x) & ALL(d):[d e x => d e qp]

& EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]

Join, 42, 34

As Required:

44 ALL(a):[a e rp

=> Set(a) & ALL(d):[d e a => d e qp]

& EXIST(b):b e a

& EXIST(b):[b e qp & ~b e a]

& ALL(b):[b e a => ALL(c):[c e qp => [c c e a]]]

& ALL(b):[b e a => EXIST(c):[c e a & b<c]]]

4 Conclusion, 23

'<='

Prove: ALL(a):[Set(a) & ALL(d):[d e a => d e qp]

& EXIST(b):b e a

& EXIST(b):[b e qp & ~b e a]

& ALL(b):[b e a => ALL(c):[c e qp => [c c e a]]]

& ALL(b):[b e a => EXIST(c):[c e a & b<c]]

=> a e rp]

Suppose...

45 Set(x) & ALL(d):[d e x => d e qp]

& EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]

Premise

46 Set(x)

Split, 45

47 ALL(d):[d e x => d e qp]

Split, 45

48 EXIST(b):b e x

Split, 45

49 EXIST(b):[b e qp & ~b e x]

Split, 45

50 ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

Split, 45

51 ALL(b):[b e x => EXIST(c):[c e x & b<c]]

Split, 45

Apply definition of rp

52 x e rp <=> x e pqp & [EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]]

U Spec, 22

53 [x e rp => x e pqp & [EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]]]

& [x e pqp & [EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]] => x e rp]

Iff-And, 52

54 x e rp => x e pqp & [EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]]

Split, 53

Sufficient For: x e rp

55 x e pqp & [EXIST(b):b e x

& EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]] => x e rp

Split, 53

Apply definition of pqp

56 x e pqp <=> Set(x) & ALL(d):[d e x => d e qp]

U Spec, 18

57 [x e pqp => Set(x) & ALL(d):[d e x => d e qp]]

& [Set(x) & ALL(d):[d e x => d e qp] => x e pqp]

Iff-And, 56

58 x e pqp => Set(x) & ALL(d):[d e x => d e qp]

Split, 57

Sufficient For: x e pqp

59 Set(x) & ALL(d):[d e x => d e qp] => x e pqp

Split, 57

60 Set(x) & ALL(d):[d e x => d e qp]

Join, 46, 47

61 x e pqp

Detach, 59, 60

Joing results...

62 EXIST(b):b e x & EXIST(b):[b e qp & ~b e x]

Join, 48, 49

63 EXIST(b):b e x & EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

Join, 62, 50

64 EXIST(b):b e x & EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]

Join, 63, 51

65 x e pqp

& [EXIST(b):b e x & EXIST(b):[b e qp & ~b e x]

& ALL(b):[b e x => ALL(c):[c e qp => [c c e x]]]

& ALL(b):[b e x => EXIST(c):[c e x & b<c]]]

Join, 61, 64

66 x e rp

Detach, 55, 65

As Required:

67 ALL(a):[Set(a) & ALL(d):[d e a => d e qp]

& EXIST(b):b e a

& EXIST(b):[b e qp & ~b e a]

& ALL(b):[b e a => ALL(c):[c e qp => [c c e a]]]

& ALL(b):[b e a => EXIST(c):[c e a & b<c]]

=> a e rp]

4 Conclusion, 45

Joining results...

68 ALL(a):[[a e rp

=> Set(a) & ALL(d):[d e a => d e qp]

& EXIST(b):b e a

& EXIST(b):[b e qp & ~b e a]

& ALL(b):[b e a => ALL(c):[c e qp => [c c e a]]]

& ALL(b):[b e a => EXIST(c):[c e a & b<c]]] & [Set(a) & ALL(d):[d e a => d e qp]

& EXIST(b):b e a

& EXIST(b):[b e qp & ~b e a]

& ALL(b):[b e a => ALL(c):[c e qp => [c c e a]]]

& ALL(b):[b e a => EXIST(c):[c e a & b<c]]

=> a e rp]]

Join, 44, 67

Apply Iff-And Rule

69 ALL(a):[a e rp

<=> Set(a) & ALL(d):[d e a => d e qp]

& EXIST(b):b e a

& EXIST(b):[b e qp & ~b e a]

& ALL(b):[b e a => ALL(c):[c e qp => [c c e a]]]

& ALL(b):[b e a => EXIST(c):[c e a & b<c]]]

Iff-And, 68

Generalizing...

As Required:

70 EXIST(rp):ALL(a):[a e rp

<=> Set(a) & ALL(d):[d e a => d e qp]

& EXIST(b):b e a

& EXIST(b):[b e qp & ~b e a]

& ALL(b):[b e a => ALL(c):[c e qp => [c c e a]]]

& ALL(b):[b e a => EXIST(c):[c e a & b<c]]]

E Gen, 69