Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.
|
|
|
|
Peano-like Axioms for the Integers in DC Proof
Posted:
Feb 22, 2013 9:57 AM
|
|
For the natural numbers, we can define a set, an element of that set (the 0 or 1) and a function on that set (the successor function as in Peano's Axioms). In my previous posting here, "Natural numbers embedded in other sets," I posted a 112 line formal proof that natural number-like structures are embedded in every set on which there is defined an injective, non-surjective function. In a similar way, I have been able to show integer-like structures are embedded in other, much simpler structures.
For the integers, we can define 3 sets (z, zright, zleft), an element common to each (the 0), and a bijection (next) on one of those sets (z) as well as its inverse (next').
In the notation of DC Proof 2.0 (with epsilon mapped to "@" and informal comments before each axiom), the 14 Peano-like axioms for the integers are:
z is a set
1 Set(z)
zright is a set
2 Set(zright)
zleft is a set
3 Set(zleft)
next is a function mapping z to itself
4 ALL(a):[a @ z => next(a) @ z]
next' is also a function mapping z to itself
5 ALL(a):[a @ z => next'(a) @ z]
6 0 @ z
z is the union of zright and zleft
7 ALL(a):[a @ z => a @ zright | a @ zleft]
0 is the only common element of zright and zleft
8 ALL(a):[a @ zright & a @ zleft <=> a=0]
next' is the inverse of next
9 ALL(a):ALL(b):[a @ z & b @ z => [next'(a)=b <=> next(b)=a]]
next is closed on zright
10 ALL(a):[a @ zright => next(a) @ zright]
0 has no pre-image in zright under next
11 ALL(a):[a @ zright => ~next(a)=0]
next' is closed on zleft
12 ALL(a):[a @ zleft => next'(a) @ zleft]
0 has no pre-image in zleft under next'
13 ALL(a):[a @ zleft => ~next'(a)=0]
The principle of mathematical induction for integers
14 ALL(p):[Set(p)
& ALL(a):[a @ p => a @ z]
& 0 @ p
& ALL(a):[a @ p => next(a) @ p]
& ALL(a):[a @ p => next'(a) @ p]
=> ALL(a):[a @ z => a @ p]]
The most interesting part of this exercise, for me, was that I was able to formally construct z, zright, zleft, next and next' from two arbitrary sets defined as follows:
right is a set
1 Set(right)
left is a set
2 Set(left)
0 is the only element in common to both right and left
3 ALL(a):[a @ right & a @ left <=> a=0]
f is an injective (1-to-1) function defined on right
4 ALL(a):[a @ right => f(a) @ right]
5 ALL(a):ALL(b):[a @ right & b @ right => [f(a)=f(b) => a=b]]
0 has no pre-image in right under f
6 ALL(a):[a @ right => ~f(a)=0]
g is an injective (1-to-1) function defined on left
7 ALL(a):[a @ left => g(a) @ left]
8 ALL(a):ALL(b):[a @ left & b @ left => [g(a)=g(b) => a=b]]
0 has no pre-image in left under g
9 ALL(a):[a @ left => ~g(a)=0]
Dan
Download my DC Proof 2.0 software at http://www.dcproof.com
Visit my new math blog at http://www.dcproof.wordpress.com
|
|
|
|
