Peano's Axioms from an Infinite Set

THEOREM

*******

Let x be an infinite set. There exists a subset n of x, function f: n --> n and x0 in n such that (n,f,x0) satisfies Peano's axioms (PA1-5).

Lines

-----

13-39 Define f: x --> x

40-42 Define x0

43-46 Construct subset n of x

47-57 PA1: x0 e n

59-84 PA2: f is closed on n

93-107 PA3: f is injective on n

108-113 PA4: There is no pre-image of x0 in n under f

114-141 PA5: Induction holds on n using f as the successor function and x0 as the "first" element

142-151 Generalizing

This proof was written and machine-verified with the aid of the author's DC Proof 2.0 software

available at http://www.dcproof.com

DEFINITIONS

***********

Define: Infinite

1 ALL(a):[Infinite(a) <=> EXIST(f):[ALL(b):[b e a => f(b) e a] & [Injective(f,a,a)
& ~Surjective(f,a,a)]]]

Axiom

Define: Injective

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

Axiom

Define: Surjective

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

Axiom

PROOF

*****

Suppose x is an infinite set

4 Set(x) & Infinite(x)

Premise

5 Set(x)

Split, 4

6 Infinite(x)

Split, 4

Apply definition of Infinite

7 Infinite(x) <=> EXIST(f):[ALL(b):[b e x => f(b) e x] & [Injective(f,x,x)
& ~Surjective(f,x,x)]]

U Spec, 1

8 [Infinite(x) => EXIST(f):[ALL(b):[b e x => f(b) e x] & [Injective(f,x,x)
& ~Surjective(f,x,x)]]]

& [EXIST(f):[ALL(b):[b e x => f(b) e x] & [Injective(f,x,x) & ~Surjective(f,x,x)]]
=> Infinite(x)]

Iff-And, 7

9 Infinite(x) => EXIST(f):[ALL(b):[b e x => f(b) e x] & [Injective(f,x,x)
& ~Surjective(f,x,x)]]

Split, 8

10 EXIST(f):[ALL(b):[b e x => f(b) e x] & [Injective(f,x,x) & ~Surjective(f,x,x)]]

=> Infinite(x)

Split, 8

11 EXIST(f):[ALL(b):[b e x => f(b) e x] & [Injective(f,x,x) & ~Surjective(f,x,x)]]

Detach, 9, 6

12 ALL(b):[b e x => f(b) e x] & [Injective(f,x,x) & ~Surjective(f,x,x)]

E Spec, 11

13 ALL(b):[b e x => f(b) e x]

Split, 12

14 Injective(f,x,x) & ~Surjective(f,x,x)

Split, 12

15 Injective(f,x,x)

Split, 14

16 ~Surjective(f,x,x)

Split, 14

Apply definition of Injective

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

U Spec, 2

18 ALL(b):[Injective(f,x,b) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]

U Spec, 17

19 Injective(f,x,x) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

U Spec, 18

20 [Injective(f,x,x) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]

& [ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injective(f,x,x)]

Iff-And, 19

21 Injective(f,x,x) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

Split, 20

22 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injective(f,x,x)

Split, 20

f is injective

23 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]

Detach, 21, 15

Apply definition of Surjective

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

U Spec, 3

25 ALL(b):[Surjective(f,x,b) <=> ALL(c):[c e b => EXIST(d):[d e x & f(d)=c]]]

U Spec, 24

26 Surjective(f,x,x) <=> ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]]

U Spec, 25

27 [Surjective(f,x,x) => ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]]]

& [ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]] => Surjective(f,x,x)]

Iff-And, 26

28 Surjective(f,x,x) => ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]]

Split, 27

29 ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]] => Surjective(f,x,x)

Split, 27

Necessary for ~Surjective

30 ~Surjective(f,x,x) => ~ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]]

Contra, 29

31 ~ALL(c):[c e x => EXIST(d):[d e x & f(d)=c]]

Detach, 30, 16

32 ~~EXIST(c):~[c e x => EXIST(d):[d e x & f(d)=c]]

Quant, 31

33 EXIST(c):~[c e x => EXIST(d):[d e x & f(d)=c]]

Rem DNeg, 32

34 EXIST(c):~~[c e x & ~EXIST(d):[d e x & f(d)=c]]

Imply-And, 33

35 EXIST(c):[c e x & ~EXIST(d):[d e x & f(d)=c]]

Rem DNeg, 34

36 EXIST(c):[c e x & ~~ALL(d):~[d e x & f(d)=c]]

Quant, 35

37 EXIST(c):[c e x & ALL(d):~[d e x & f(d)=c]]

Rem DNeg, 36

38 EXIST(c):[c e x & ALL(d):~~[d e x => ~f(d)=c]]

Imply-And, 37

39 EXIST(c):[c e x & ALL(d):[d e x => ~f(d)=c]]

Rem DNeg, 38

40 x0 e x & ALL(d):[d e x => ~f(d)=x0]

E Spec, 39

Define: x0

41 x0 e x

Split, 40

42 ALL(d):[d e x => ~f(d)=x0]

Split, 40

Construct subset n of x

Apply Subset Axiom

43 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e x & ALL(b):[Set(b)

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

& x0 e b

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

=> a e b]]]

Subset, 5

44 Set(n) & ALL(a):[a e n <=> a e x & ALL(b):[Set(b)

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

& x0 e b

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

=> a e b]]

E Spec, 43

Define: n

45 Set(n)

Split, 44

46 ALL(a):[a e n <=> a e x & ALL(b):[Set(b)

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

& x0 e b

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

=> a e b]]

Split, 44

Prove: x0 e n (PA1)

Apply definition of n

47 x0 e n <=> x0 e x & ALL(b):[Set(b)

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

& x0 e b

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

=> x0 e b]

U Spec, 46

48 [x0 e n => x0 e x & ALL(b):[Set(b)

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

& x0 e b

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

=> x0 e b]]

& [x0 e x & ALL(b):[Set(b)

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

& x0 e b

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

=> x0 e b] => x0 e n]

Iff-And, 47

49 x0 e n => x0 e x & ALL(b):[Set(b)

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

& x0 e b

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

=> x0 e b]

Split, 48

Sufficient: For x0 in n

50 x0 e x & ALL(b):[Set(b)

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

& x0 e b

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

=> x0 e b] => x0 e n

Split, 48

51 Set(q)

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

& x0 e q

& ALL(c):[c e q => f(c) e q]

Premise

52 Set(q)

Split, 51

53 ALL(c):[c e q => c e x]

Split, 51

54 x0 e q

Split, 51

55 ALL(b):[Set(b)

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

& x0 e b

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

=> x0 e b]

4 Conclusion, 51

56 x0 e x

& ALL(b):[Set(b)

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

& x0 e b

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

=> x0 e b]

Join, 41, 55

PA1

***

57 x0 e n

Detach, 50, 56

Prove: ALL(a):[a e n => f(a) e n] (PA2)

Suppose...

58 t e n

Premise

Apply definition of n

59 t e n <=> t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]

U Spec, 46

60 [t e n => t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]]

& [t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b] => t e n]

Iff-And, 59

61 t e n => t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]

Split, 60

62 t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b] => t e n

Split, 60

63 t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]

Detach, 61, 58

64 t e x

Split, 63

65 ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]

Split, 63

Apply definition n

66 f(t) e n <=> f(t) e x & ALL(b):[Set(b)

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

& x0 e b

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

=> f(t) e b]

U Spec, 46

67 [f(t) e n => f(t) e x & ALL(b):[Set(b)

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

& x0 e b

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

=> f(t) e b]]

& [f(t) e x & ALL(b):[Set(b)

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

& x0 e b

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

=> f(t) e b] => f(t) e n]

Iff-And, 66

68 f(t) e n => f(t) e x & ALL(b):[Set(b)

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

& x0 e b

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

=> f(t) e b]

Split, 67

Sufficient: For f(t) e n

69 f(t) e x & ALL(b):[Set(b)

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

& x0 e b

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

=> f(t) e b] => f(t) e n

Split, 67

Apply previous result

70 t e x => f(t) e x

U Spec, 13

71 f(t) e x

Detach, 70, 64

Prove: ALL(b):[Set(b)

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

& x0 e b

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

=> f(t) e b]

Suppose...

72 Set(q)

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

& x0 e q

& ALL(c):[c e q => f(c) e q]

Premise

73 Set(q)

Split, 72

74 ALL(c):[c e q => c e x]

Split, 72

75 x0 e q

Split, 72

76 ALL(c):[c e q => f(c) e q]

Split, 72

77 t e q => f(t) e q

U Spec, 76

Apply previous result

78 Set(q)

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

& x0 e q

& ALL(c):[c e q => f(c) e q]

=> t e q

U Spec, 65

79 t e q

Detach, 78, 72

80 f(t) e q

Detach, 77, 79

As Required:

81 ALL(b):[Set(b)

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

& x0 e b

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

=> f(t) e b]

4 Conclusion, 72

82 f(t) e x

& ALL(b):[Set(b)

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

& x0 e b

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

=> f(t) e b]

Join, 71, 81

83 f(t) e n

Detach, 69, 82

PA2 f is closed on n

***

84 ALL(a):[a e n => f(a) e n]

4 Conclusion, 58

Prove: n is a subset of x

Suppose...

85 t e n

Premise

86 t e n <=> t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]

U Spec, 46

87 [t e n => t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]]

& [t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b] => t e n]

Iff-And, 86

88 t e n => t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]

Split, 87

89 t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b] => t e n

Split, 87

90 t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]

Detach, 88, 85

91 t e x

Split, 90

As Required:

n is a subset of x

92 ALL(a):[a e n => a e x]

4 Conclusion, 85

Prove: ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]] (PA3)

Suppose...

93 t e n & u e n

Premise

94 t e n

Split, 93

95 u e n

Split, 93

Prove: f(t)=f(u) => t=u

Suppose...

96 f(t)=f(u)

Premise

Apply previous result

97 ALL(d):[t e x & d e x => [f(t)=f(d) => t=d]]

U Spec, 23

98 t e x & u e x => [f(t)=f(u) => t=u]

U Spec, 97

99 t e n => t e x

U Spec, 92

100 t e x

Detach, 99, 94

101 u e n => u e x

U Spec, 92

102 u e x

Detach, 101, 95

103 t e x & u e x

Join, 100, 102

104 f(t)=f(u) => t=u

Detach, 98, 103

105 t=u

Detach, 104, 96

As Required:

106 f(t)=f(u) => t=u

4 Conclusion, 96

PA3 f is injective on n

***

107 ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]

4 Conclusion, 93

Prove: ALL(a):[a e n => ~f(a)=x0] (PA4)

Suppose...

108 t e n

Premise

109 t e x => ~f(t)=x0

U Spec, 42

110 t e n => t e x

U Spec, 92

111 t e x

Detach, 110, 108

112 ~f(t)=x0

Detach, 109, 111

PA4 x0 has no pre-image in n under f

***

113 ALL(a):[a e n => ~f(a)=x0]

4 Conclusion, 108

Prove: ALL(a):[Set(a) & ALL(b):[b e a => b e n] (PA5)

=> [x0 e a & ALL(b):[b e a => f(b) e a]

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

Suppose...

114 Set(p) & ALL(b):[b e p => b e n]

Premise

115 Set(p)

Split, 114

116 ALL(b):[b e p => b e n]

Split, 114

Prove: x0 e p & ALL(b):[b e p => f(b) e p]

=> ALL(b):[b e n => b e p]

Suppose...

117 x0 e p & ALL(b):[b e p => f(b) e p]

Premise

118 x0 e p

Split, 117

119 ALL(b):[b e p => f(b) e p]

Split, 117

Prove: ALL(b):[b e n => b e p]

Suppose...

120 t e n

Premise

Apply definition of n

121 t e n <=> t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]

U Spec, 46

122 [t e n => t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]]

& [t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b] => t e n]

Iff-And, 121

123 t e n => t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]

Split, 122

124 t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b] => t e n

Split, 122

125 t e x & ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]

Detach, 123, 120

126 t e x

Split, 125

127 ALL(b):[Set(b)

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

& x0 e b

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

=> t e b]

Split, 125

Sufficient: For t e p

128 Set(p)

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

& x0 e p

& ALL(c):[c e p => f(c) e p]

=> t e p

U Spec, 127

Prove: ALL(c):[c e p => c e x]

Suppose...

129 u e p

Premise

130 u e p => u e n

U Spec, 116

131 u e n

Detach, 130, 129

132 u e n => u e x

U Spec, 92

133 u e x

Detach, 132, 131

As Required:

134 ALL(c):[c e p => c e x]

4 Conclusion, 129

135 Set(p) & ALL(c):[c e p => c e x]

Join, 115, 134

136 Set(p) & ALL(c):[c e p => c e x] & x0 e p

Join, 135, 118

137 Set(p) & ALL(c):[c e p => c e x] & x0 e p

& ALL(b):[b e p => f(b) e p]

Join, 136, 119

138 t e p

Detach, 128, 137

As Required:

139 ALL(b):[b e n => b e p]

4 Conclusion, 120

As Required:

140 x0 e p & ALL(b):[b e p => f(b) e p]

=> ALL(b):[b e n => b e p]

4 Conclusion, 117

PA5 Induction holds on n with successor function f and "first" element x0

***

141 ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

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

4 Conclusion, 114

Joining previous results...

142 Set(n) & ALL(a):[a e n => a e x]

Join, 45, 92

143 Set(n) & ALL(a):[a e n => a e x] & x0 e n

Join, 142, 57

144 Set(n) & ALL(a):[a e n => a e x] & x0 e n

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

Join, 143, 84

145 Set(n) & ALL(a):[a e n => a e x] & x0 e n

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

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

Join, 144, 107

146 Set(n) & ALL(a):[a e n => a e x] & x0 e n

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

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

& ALL(a):[a e n => ~f(a)=x0]

Join, 145, 113

147 Set(n) & ALL(a):[a e n => a e x] & x0 e n

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

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

& ALL(a):[a e n => ~f(a)=x0]

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

=> [x0 e a & ALL(b):[b e a => f(b) e a]

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

Join, 146, 141

148 EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

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

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

& ALL(a):[a e n => ~f(a)=x0]

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

=> [x0 e a & ALL(b):[b e a => f(b) e a]

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

E Gen, 147

149 EXIST(f):EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

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

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

& ALL(a):[a e n => ~f(a)=x0]

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

=> [x0 e a & ALL(b):[b e a => f(b) e a]

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

E Gen, 148

150 EXIST(n):EXIST(f):EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

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

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

& ALL(a):[a e n => ~f(a)=x0]

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

=> [x0 e a & ALL(b):[b e a => f(b) e a]

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

E Gen, 149

As Required:

151 ALL(x):[Set(x) & Infinite(x)

=> EXIST(n):EXIST(f):EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

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

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

& ALL(a):[a e n => ~f(a)=x0]

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

=> [x0 e a & ALL(b):[b e a => f(b) e a]

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

4 Conclusion, 4