Search All of the Math Forum:

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

Topic: Number of variables needed to axiomatize first order predicate calculus?
Replies: 4   Last Post: Mar 19, 2013 11:48 PM

 Messages: [ Previous | Next ]
 Graham Cooper Posts: 4,422 Registered: 5/20/10
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.
>
> > -----------
>
>
> > 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 Counter-Example ..
running at BlockProlog.com!

I had to write my own Prolog to get a decent Trace to see how Proof By

Herc
--
www.BLoCKPROLOG.com

Date Subject Author
3/18/13 Graham Cooper
3/19/13 JT
3/19/13 Graham Cooper