INTRODUCTION
************
Following are my proposed axioms for the set of integers (modelled on Peano's Axioms for the natural numbers). Preliminary results are encouraging. Such a structure can be proven to exist given basic arithemetic on the natural numbers and the axioms of set theory (formal proofs to follow). Note, however, that these axioms make no reference to the natural numbers. (This represents a significant departure from my previous posting on this topic.)
Also included here is an "initial test" of theses axioms -- a formal proof of the following:
THEOREM
*******
No integer is its own successor. More formally:
ALL(a):[a e int => ~next(a)=a]
where
int = the set of integers
next = the successor function on the integers
OUTLINE
*******
Lines
1-18 Proposed axioms for set the of integers
19-27 Preliminary results
43-50 Base case for proof
52-76 1st inductive step (=>)
77-99 2nd inductive step (<=)
102-112 Conclusion
This formal proof was written and machine-verified with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com
PROPOSED AXIOMS
***************
int = set of integers
1 Set(int)
Axiom
right = non-negative integers
2 Set(right)
Axiom
3 ALL(a):[a e right => a e int]
Axiom
left = non-positive integers
4 Set(left)
Axiom
5 ALL(a):[a e right => a e int]
Axiom
z0 = integer zero
6 z0 e int
Axiom
int is the union of right and light
7 ALL(a):[a e int => a e right | a e left]
Axiom
z0 is the intersection of right and left
8 ALL(a):[a e int => [a e right & a e left <=> a=z0]]
Axiom
next is a function mapping int to itself
9 ALL(a):[a e int => next(a) e int]
Axiom
next is injective
10 ALL(a):ALL(b):[a e int & b e int => [next(a)=next(b) => a=b]]
Axiom
next is surjective
11 ALL(a):[a e int => EXIST(b):[b e int & next(b)=a]]
Axiom
next is closed on right
12 ALL(a):[a e right => next(a) e right]
Axiom
z0 has no predecessor in right
13 ALL(a):[a e right => ~next(a)=z0]
Axiom
One-way Induction holds on right under successor function next
14 ALL(a):[Set(a) & ALL(b):[b e a => b e right]
=> [z0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e right => b e a]]]
Axiom
The inverse of next is closed on left
15 ALL(a):ALL(b):[a e left & b e int & next(b)=a => b e left]
Axiom
z0 has no predecessor in left
16 ALL(a):ALL(b):[a e left & b e int & next(b)=a => ~b=z0]
Axiom
One-way Induction holds of left under inverse of next
17 ALL(a):[Set(a) & ALL(b):[b e a => b e left]
=> [z0 e a & ALL(b):ALL(c):[b e a & c e int & next(c)=b => c e a]
=> ALL(b):[b e left => b e a]]]
Axiom
Two-way Induction holds on int under successor function next
18 ALL(a):[Set(a) & ALL(b):[b e a => b e int]
=> [z0 e a & ALL(b):[b e int => [b e a <=> next(b) e a]]
=> ALL(b):[b e int => b e a]]]
Axiom
PRELIMINARIES
*************
Prove: z0 e right and z0 e left
Apply Axiom 8
19 z0 e int => [z0 e right & z0 e left <=> z0=z0]
U Spec, 8
Apply Detachment Rule
20 z0 e right & z0 e left <=> z0=z0
Detach, 19, 6
21 [z0 e right & z0 e left => z0=z0]
& [z0=z0 => z0 e right & z0 e left]
Iff-And, 20
Splitting this result...
22 z0 e right & z0 e left => z0=z0
Split, 21
23 z0=z0 => z0 e right & z0 e left
Split, 21
24 z0=z0
Reflex
Apply Detachment Rule
25 z0 e right & z0 e left
Detach, 23, 24
As Required:
26 z0 e right
Split, 25
27 z0 e left
Split, 25
First, apply Subset Axiom to construct the subset p of integers that are not equal to their successors.
We will prove by 2-way induction that all integers are in this set.
28 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e int & ~next(a)=a]]
Subset, 1
29 Set(p) & ALL(a):[a e p <=> a e int & ~next(a)=a]
E Spec, 28
Define: p
30 Set(p)
Split, 29
31 ALL(a):[a e p <=> a e int & ~next(a)=a]
Split, 29
Apply two-way induction axiom
32 Set(p) & ALL(b):[b e p => b e int]
=> [z0 e p & ALL(b):[b e int => [b e p <=> next(b) e p]]
=> ALL(b):[b e int => b e p]]
U Spec, 18
Prove: ALL(b):[b e p => b e int]
Suppose...
33 x e p
Premise
Apply definition of p
34 x e p <=> x e int & ~next(x)=x
U Spec, 31
35 [x e p => x e int & ~next(x)=x]
& [x e int & ~next(x)=x => x e p]
Iff-And, 34
36 x e p => x e int & ~next(x)=x
Split, 35
37 x e int & ~next(x)=x => x e p
Split, 35
Apply Detachment Rule
38 x e int & ~next(x)=x
Detach, 36, 33
39 x e int
Split, 38
As Required:
40 ALL(b):[b e p => b e int]
4 Conclusion, 33
Joining results...
41 Set(p) & ALL(b):[b e p => b e int]
Join, 30, 40
Sufficient: For ALL(b):[b e int => b e p]
Apply Detachment Rule
42 z0 e p & ALL(b):[b e int => [b e p <=> next(b) e p]]
=> ALL(b):[b e int => b e p]
Detach, 32, 41
BASE CASE
*********
Prove: z0 e p
Apply definition of p
43 z0 e p <=> z0 e int & ~next(z0)=z0
U Spec, 31
44 [z0 e p => z0 e int & ~next(z0)=z0]
& [z0 e int & ~next(z0)=z0 => z0 e p]
Iff-And, 43
45 z0 e p => z0 e int & ~next(z0)=z0
Split, 44
Sufficient: For z0 e p
46 z0 e int & ~next(z0)=z0 => z0 e p
Split, 44
Apply Axiom 13
47 z0 e right => ~next(z0)=z0
U Spec, 13
48 ~next(z0)=z0
Detach, 47, 26
Joining results...
49 z0 e int & ~next(z0)=z0
Join, 6, 48
As Required:
50 z0 e p
Detach, 46, 49
INDUCTIVE STEPS
***************
Suppose...
51 x e int
Premise
1ST INDUCTIVE STEP (=>)
***********************
Prove: x e p => next(x) e p
Suppose...
52 x e p
Premise
Apply definition of p
53 x e p <=> x e int & ~next(x)=x
U Spec, 31
54 [x e p => x e int & ~next(x)=x]
& [x e int & ~next(x)=x => x e p]
Iff-And, 53
55 x e p => x e int & ~next(x)=x
Split, 54
56 x e int & ~next(x)=x => x e p
Split, 54
Apply Detachment Rule
57 x e int & ~next(x)=x
Detach, 55, 52
58 x e int
Split, 57
59 ~next(x)=x
Split, 57
Apply definition of p
60 next(x) e p <=> next(x) e int & ~next(next(x))=next(x)
U Spec, 31
61 [next(x) e p => next(x) e int & ~next(next(x))=next(x)]
& [next(x) e int & ~next(next(x))=next(x) => next(x) e p]
Iff-And, 60
62 next(x) e p => next(x) e int & ~next(next(x))=next(x)
Split, 61
Sufficient: For next(x) e p
63 next(x) e int & ~next(next(x))=next(x) => next(x) e p
Split, 61
Prove: next(x) e int
Apply Axiom 9
64 x e int => next(x) e int
U Spec, 9
65 next(x) e int
Detach, 64, 51
Prove: ~next(next(x))=next(x)
Suppose to the contrary...
66 next(next(x))=next(x)
Premise
Apply Axiom 10
67 ALL(b):[next(x) e int & b e int => [next(next(x))=next(b) => next(x)=b]]
U Spec, 10
68 next(x) e int & x e int => [next(next(x))=next(x) => next(x)=x]
U Spec, 67
Joining results...
69 next(x) e int & x e int
Join, 65, 51
Apply Detachment Rule
70 next(next(x))=next(x) => next(x)=x
Detach, 68, 69
Apply Detachment Rule
71 next(x)=x
Detach, 70, 66
Obtain contradiction
Joining results...
72 next(x)=x & ~next(x)=x
Join, 71, 59
As Required:
73 ~next(next(x))=next(x)
4 Conclusion, 66
Joining results...
74 next(x) e int & ~next(next(x))=next(x)
Join, 65, 73
Apply Detachment Rule
75 next(x) e p
Detach, 63, 74
As Required:
76 x e p => next(x) e p
4 Conclusion, 52
2ND INDUCTIVE STEP (<=)
***********************
Prove: next(x) e p => x e p
Suppose...
77 next(x) e p
Premise
Apply definition of p
78 next(x) e p <=> next(x) e int & ~next(next(x))=next(x)
U Spec, 31
79 [next(x) e p => next(x) e int & ~next(next(x))=next(x)]
& [next(x) e int & ~next(next(x))=next(x) => next(x) e p]
Iff-And, 78
80 next(x) e p => next(x) e int & ~next(next(x))=next(x)
Split, 79
81 next(x) e int & ~next(next(x))=next(x) => next(x) e p
Split, 79
Apply Detachment Rule
82 next(x) e int & ~next(next(x))=next(x)
Detach, 80, 77
83 next(x) e int
Split, 82
84 ~next(next(x))=next(x)
Split, 82
Apply definition of p
85 x e p <=> x e int & ~next(x)=x
U Spec, 31
86 [x e p => x e int & ~next(x)=x]
& [x e int & ~next(x)=x => x e p]
Iff-And, 85
87 x e p => x e int & ~next(x)=x
Split, 86
Sufficient for: x e p
88 x e int & ~next(x)=x => x e p
Split, 86
Prove: ~next(x)=x
Suppose to the contrary...
89 next(x)=x
Premise
90 ~next(x)=next(x)
Substitute, 89, 84
91 next(x)=next(x)
Reflex
Obtain contradiction
Joining results...
92 next(x)=next(x) & ~next(x)=next(x)
Join, 91, 90
As Required:
93 ~next(x)=x
4 Conclusion, 89
Joining results...
94 x e int & ~next(x)=x
Join, 51, 93
Apply Detachment Rule
95 x e p
Detach, 88, 94
As Required:
96 next(x) e p => x e p
4 Conclusion, 77
Joining results
97 [x e p => next(x) e p] & [next(x) e p => x e p]
Join, 76, 96
98 x e p <=> next(x) e p
Iff-And, 97
As Required:
99 ALL(b):[b e int => [b e p <=> next(b) e p]]
4 Conclusion, 51
Joining results...
100 z0 e p
& ALL(b):[b e int => [b e p <=> next(b) e p]]
Join, 50, 99
Apply Detachment Rule
As Required:
101 ALL(b):[b e int => b e p]
Detach, 42, 100
Prove: ALL(a):[a e int => ~next(a)=a]
Suppose...
102 x e int
Premise
Apply previous result
103 x e int => x e p
U Spec, 101
104 x e p
Detach, 103, 102
105 x e p <=> x e int & ~next(x)=x
U Spec, 31
106 [x e p => x e int & ~next(x)=x]
& [x e int & ~next(x)=x => x e p]
Iff-And, 105
107 x e p => x e int & ~next(x)=x
Split, 106
108 x e int & ~next(x)=x => x e p
Split, 106
Apply Detachment Rule
109 x e int & ~next(x)=x
Detach, 107, 104
110 x e int
Split, 109
111 ~next(x)=x
Split, 109
As Required:
112 ALL(a):[a e int => ~next(a)=a]
4 Conclusion, 102