Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.



Re: Number of variables needed to axiomatize first order predicate calculus?
Posted:
Mar 18, 2013 10:24 PM


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



