Date: Mar 18, 2013 10:24 PM
Author: Graham Cooper
Subject: Re: Number of variables needed to axiomatize first order predicate calculus?
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