Search All of the Math Forum:

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

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

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

 Messages: [ Previous | Next ]
 JT Posts: 1,448 Registered: 4/7/12
Re: Number of variables needed to axiomatize first order predicate calculus?
Posted: Mar 19, 2013 4:50 AM

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