
Re: Number of variables needed to axiomatize first order predicate calculus?
Posted:
Mar 19, 2013 11:48 PM


On Mar 19, 6:50 pm, JT <jonas.thornv...@gmail.com> wrote: > On 19 mar, 03:24, Graham Cooper <grahamcoop...@gmail.com> wrote: > > > On Mar 19, 10:40 am, George Greene <gree...@email.unc.edu> wrote: > > > > On Mar 18, 7:39 pm, Frederick Williams <freddywilli...@btinternet.com> > > > wrote: > > > > > I don't see how you will get far without modus ponens. > > > > Well, I see your point that unless everything is going to be a direct > > > instance of some single axiom, > > > you have to have an inference rule that produces a consequence from an > > > input. > > > But the question still arises, why isn't that > ? > > > You sort of need modus ponens and a deduction theorem to get from > > > A / B to A > B, but doesn't it take more "variables" just to bridge > > > that modality? > > > > It just seems to me you are operating from a textbook with a framework > > > that has > > > not been presented to anyone who is not also reading that textbook, > > > and that > > > is ITself in need of some defense. > > > If you want to forward chain or backward chain via inference rules > > > you're going to need another syntax symbol than > > > > If not in the inference rule itself, then in a separate control module > > which usually has modus ponens, cut elimination or resolution. > > > MP can emulate those last 2 as inference rules. > > >  > > > e.g. in PROLOG instead of > > > not(not(X)) : thm(X). > > > use > > > if( X , not(not(X))). > > and > > thm(R) : if(L,R) , thm(L) [MP] > > >  > > > Both methods have a : somewhere > > > You just put thm(X) around a naked theorem X in PROLOG. > > > Herc > > www.BLoCKPROLOG.com > > Is your code microprolog compatible i just downloaded a ZX emulator? >
This should run on any bog standard Prolog as I only use atomic predicates.
tru(t). not(f).
and(X,Y) : tru(X),tru(Y). and(X,not(Y)) : tru(X),not(Y). and(not(X),Y) : not(X),tru(Y). and(not(X),not(Y)) : not(X),not(Y).
even(0). not(and( even(X) , not(even(s(s(X)))) )). e(A, evens) : tru(even(A)). tru(even(X)) : even(X).
tru(e(A,S)) : e(A,S).
tru(R) : not(and(L,not(R))) , tru(L).
tru( e( s(s(s(s(0)))) , evens ))?

Give me another month and I'll get a full theorem prover with Proof by Contradiction and Proof by Induction, Proof by CounterExample .. running at BlockProlog.com!
I had to write my own Prolog to get a decent Trace to see how Proof By Contradiction works!
Herc  www.BLoCKPROLOG.com

