The Math Forum

Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Math Forum » Discussions » sci.math.* » sci.math

Topic: Peano-like Axioms for the Integers in DC Proof
Replies: 0  

Advanced Search

Back to Topic List Back to Topic List  
Dan Christensen

Posts: 6,540
Registered: 7/9/08
Peano-like Axioms for the Integers in DC Proof
Posted: Feb 22, 2013 9:57 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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]

Download my DC Proof 2.0 software at
Visit my new math blog at

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© The Math Forum at NCTM 1994-2017. All Rights Reserved.