Date: Feb 23, 2013 12:53 AM
Author: Graham Cooper
Subject: Re: Peano-like Axioms for the Integers in DC Proof

> I don't know if they are anything new, but I have presented a set of axioms for the integers based on a clearly defined successor function. It differs considerably from the usual presentations that you see online. As such, I thought readers might be interested.
> Also, I'm not sure how these other sets of axioms were arrived at other than simply being as a wishlist of requirements for integer arithmetic that just seems to work.

And they DO work, as is!

nat(s(X)) :- nat(X).

even(s(s(X))) :- even(X).

odd(s(s(X))) :- odd(X).

e(A,nats) :- nat(A).
e(A,evens) :- even(A).
e(A,odds) :- odd(A).

insect(S1,S2) :- e(A,S1),e(A,S2).

?- insect(nats,evens).
?- insect(nats,odds).

This will return TRUE TRUE on any PROLOG machine.


?- e(A, nats) , e(A, evens)

will return

A = 0
A = s(s(0))
A = s(s(s(s(0))))
A = s(s(s(s(s(s(0))))))


?- e(A,nats) , e(A,odds)

will return

A = s(0)
A = s(s(s(0)))
A = s(s(s(s(s(0)))))
A = s(s(s(s(s(s(s(0)))))))

NOTE: ?-insect( odds, evens ) will CRASH!

I need to get a TRACE working to see how Prolog solves simultaneous


My axioms, however, were justified by the  application of formal
axioms and rules of logic and set theory beginning with relatively
simple structures as I have described here. I show that that an
integer-like structure with its own a principle of mathematical
induction is actually embedded in such simple structures. Admit it,
Charlie, that's pretty cool!

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]]


So succ(X) is next(X)
and right is 1,2,3,4...
and left is -1,-2,-3,-4....

I like how you define the Domain z for the inductive predicate

& ALL(a):[a @ p => a @ z]
=> ALL(a):[a @ z => a @ p]]