> > 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.
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)
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 equations..
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]]