
Re: Peanolike Axioms for the Integers in DC Proof
Posted:
Feb 24, 2013 5:39 PM


On Feb 25, 7:35 am, Dan Christensen <Dan_Christen...@sympatico.ca> wrote:
> > How do you rate Peano's attempt? > > It was a real breakthrough in its day, but it was a essentially an exercise in pattern recognition: Here are some facts about the natural numbers from which it may be possible to derive all others. What I have done differently is to derive these facts/axioms (including induction) starting with nothing more than assuming that there exists an injective fuction defined on a set
AND 2nd ORDER LOGIC!
[DAN]  I make no claim that it is firstorder.
...
Sure, given ALL(X) ...formula..
it's so easy!

This just uses DOUBLE VARIABLE NAME COMPATIBLE BINDING
and THE COMPUTER SEARCHES for the Proofs using only 10 lines!
EG. Are all Nats Even?
nat(0). nat(s(X)) : nat(X).
even(0). even(s(s(X))) : even(X).
odd(s(0)). 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).
**** QUERY NOT(ALL(NATS are EVEN)) ***
? !(subset( nats , evens )) >>!(!insect((nats, !(evens)). >> insect(nats,odds). >> TRUE
? e(A,nats) , e(A,odds)
A = s(0)
The 10 lines of PROLOG can find the counterexample NUMBER 1!
This *pattern matching*
e(A,nats) : nat(A).
is an INTERFACE from 4GL "WHAT IF" requests to 3GL recursive programs in a set theoretic framework.
The SCOPE of syntactic proof checkers tends to be limited to meta facts about the theory itself.
Herc  www.BLoCKPROLOG.com

