INTRODUCTION
************
I propose the following axioms for ultrafinist number theory.
Informally, we have n = {0, 1, 2, ... max}. Not ruled out is the possibility of max = 0 and n = {0}.
'next' is a partial function on n analogous to the Peano's successor function.
'(x,y) e next' means y is the successor of x, or x is the predecessor of y.
As a test, I prove by induction that no number is its own succesor, i.e. ALL(a):[a e n => ~(a,a) e next]
Interestingly, this proof makes reference to max.
(This formal proof was prepared with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com )
THE AXIOMS
**********
n is a set
1 Set(n)
Axiom
2 0 e n
Axiom
3 max e n
Axiom
next is a set of ordered pairs of elements of n
4 Set'(next)
Axiom
5 ALL(a):ALL(b):[(a,b) e next => a e n & b e n]
Axiom
0 has no predecessor
6 ALL(a):[a e n => ~(a,0) e next]
Axiom
max has no successor
7 ALL(a):[a e n => ~(max,a) e next]
Axiom
All numbers but max have a successor
8 ALL(a):[a e n => [~a=max => EXIST(b):[b e n & (a,b) e next]]]
Axiom
If a number has a successor, that successor is unique.
9 ALL(a):ALL(b):ALL(c):[(a,b) e next & (a,c) e next => b=c]
Axiom
If numbers x and y have the same successors, then x = y.
10 ALL(a):ALL(b):ALL(c):ALL(d):[(a,b) e next & (c,d) e next => [b=d => a=c]]
Axiom
Induction
11 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => ALL(c):[(b,c) e next => c e a]]
=> ALL(b):[b e n => b e a]]]
Axiom
PROOF
*****
Apply Subset Axiom (for inductive proof)
12 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & ~(a,a) e next]]
Subset, 1
13 Set(p) & ALL(a):[a e p <=> a e n & ~(a,a) e next]
E Spec, 12
Define: p
14 Set(p)
Split, 13
p is the subset on n satsifying the required condition
15 ALL(a):[a e p <=> a e n & ~(a,a) e next]
Split, 13
Apply inducton axiom for set p
16 Set(p) & ALL(b):[b e p => b e n]
=> [0 e p & ALL(b):[b e p => ALL(c):[(b,c) e next => c e p]]
=> ALL(b):[b e n => b e p]]
U Spec, 11
Prove: ALL(b):[b e p => b e n] i.e. p is a subset of n
Suppose...
17 x e p
Premise
Apply definition of p
18 x e p <=> x e n & ~(x,x) e next
U Spec, 15
19 [x e p => x e n & ~(x,x) e next]
& [x e n & ~(x,x) e next => x e p]
Iff-And, 18
20 x e p => x e n & ~(x,x) e next
Split, 19
21 x e n & ~(x,x) e next => x e p
Split, 19
22 x e n & ~(x,x) e next
Detach, 20, 17
23 x e n
Split, 22
As Required:
24 ALL(b):[b e p => b e n]
4 Conclusion, 17
Joining results...
25 Set(p) & ALL(b):[b e p => b e n]
Join, 14, 24
Sufficient: For ALL(b):[b e n => b e p]
26 0 e p & ALL(b):[b e p => ALL(c):[(b,c) e next => c e p]]
=> ALL(b):[b e n => b e p]
Detach, 16, 25
Prove: 0 e p
Apply definition of p
27 0 e p <=> 0 e n & ~(0,0) e next
U Spec, 15
28 [0 e p => 0 e n & ~(0,0) e next]
& [0 e n & ~(0,0) e next => 0 e p]
Iff-And, 27
29 0 e p => 0 e n & ~(0,0) e next
Split, 28
30 0 e n & ~(0,0) e next => 0 e p
Split, 28
31 0 e n => ~(0,0) e next
U Spec, 6
32 ~(0,0) e next
Detach, 31, 2
33 0 e n & ~(0,0) e next
Join, 2, 32
As Required:
34 0 e p
Detach, 30, 33
Prove: ALL(b):[b e p => ALL(c):[(b,c) e next => c e p]]
Suppose...
35 x e p
Premise
Apply definition of p
36 x e p <=> x e n & ~(x,x) e next
U Spec, 15
37 [x e p => x e n & ~(x,x) e next]
& [x e n & ~(x,x) e next => x e p]
Iff-And, 36
38 x e p => x e n & ~(x,x) e next
Split, 37
39 x e n & ~(x,x) e next => x e p
Split, 37
40 x e n & ~(x,x) e next
Detach, 38, 35
41 x e n
Split, 40
42 ~(x,x) e next
Split, 40
Prove: ALL(c):[(x,c) e next => c e p]
Suppose...
43 (x,x') e next
Premise
Apply definition of p
44 x' e p <=> x' e n & ~(x',x') e next
U Spec, 15
45 [x' e p => x' e n & ~(x',x') e next]
& [x' e n & ~(x',x') e next => x' e p]
Iff-And, 44
46 x' e p => x' e n & ~(x',x') e next
Split, 45
Sufficient: For x' e p
47 x' e n & ~(x',x') e next => x' e p
Split, 45
48 ALL(b):[(x,b) e next => x e n & b e n]
U Spec, 5
49 (x,x') e next => x e n & x' e n
U Spec, 48
50 x e n & x' e n
Detach, 49, 43
51 x e n
Split, 50
52 x' e n
Split, 50
Prove: ~(x',x') e next
Suppose to the contrary...
53 (x',x') e next
Premise
Apply axiom
54 ALL(b):ALL(c):ALL(d):[(x,b) e next & (c,d) e next => [b=d => x=c]]
U Spec, 10
55 ALL(c):ALL(d):[(x,x') e next & (c,d) e next => [x'=d => x=c]]
U Spec, 54
56 ALL(d):[(x,x') e next & (x',d) e next => [x'=d => x=x']]
U Spec, 55
57 (x,x') e next & (x',x') e next => [x'=x' => x=x']
U Spec, 56
58 (x,x') e next & (x',x') e next
Join, 43, 53
59 x'=x' => x=x'
Detach, 57, 58
60 x'=x'
Reflex
61 x=x'
Detach, 59, 60
62 ~(x',x') e next
Substitute, 61, 42
Obtain the contradiction...
63 (x',x') e next & ~(x',x') e next
Join, 53, 62
As Required:
64 ~(x',x') e next
4 Conclusion, 53
65 x' e n & ~(x',x') e next
Join, 52, 64
66 x' e p
Detach, 47, 65
As Required:
67 ALL(c):[(x,c) e next => c e p]
4 Conclusion, 43
As Required:
68 ALL(b):[b e p => ALL(c):[(b,c) e next => c e p]]
4 Conclusion, 35
Joining results...
69 0 e p
& ALL(b):[b e p => ALL(c):[(b,c) e next => c e p]]
Join, 34, 68
70 ALL(b):[b e n => b e p]
Detach, 26, 69
Prove: ALL(a):[a e n => ~(a,a) e next]
Suppose...
71 x e n
Premise
Apply previous result
72 x e n => x e p
U Spec, 70
73 x e p
Detach, 72, 71
74 x e p <=> x e n & ~(x,x) e next
U Spec, 15
75 [x e p => x e n & ~(x,x) e next]
& [x e n & ~(x,x) e next => x e p]
Iff-And, 74
76 x e p => x e n & ~(x,x) e next
Split, 75
77 x e n & ~(x,x) e next => x e p
Split, 75
78 x e n & ~(x,x) e next
Detach, 76, 73
79 x e n
Split, 78
80 ~(x,x) e next
Split, 78
As Required:
81 ALL(a):[a e n => ~(a,a) e next]
4 Conclusion, 71