Date: Nov 29, 2012 1:13 AM Author: Dan Christensen Subject: Re: PREDICATE CALCULUS 2 On Nov 29, 12:00 am, Graham Cooper <grahamcoop...@gmail.com> wrote:

> On Nov 29, 2:16 pm, Dan Christensen <Dan_Christen...@sympatico.ca>

> wrote:

>

>

>

>

>

>

>

>

>

> > On Nov 28, 8:59 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

>

> > > On Nov 29, 8:42 am, Dan Christensen <Dan_Christen...@sympatico.ca>

> > > wrote:

>

> > > > > PROLOG is just the UNIFY( f1(..) , f1(...) )

>

> > > > I would love to be proven wrong, but I don't think you will get very

> > > > far in abstract mathematics using only PROLOG. If you are still

> > > > determined to used PROLOG, you might look at Norm Megill's MetaMath

> > > > program -- the gold standard of mechanized rigour IMHO. It is very

> > > > small program and, as I understand, is based entirely on making

> > > > symbolic substitutions. Your "facts" would be facts about formuala's,

> > > > not individual objects. Just maybe you can implement it in PROLOG.

> > > > Write to Norm. He will be able to advise you. He probably knows PROLOG

> > > > as well.

>

> > > Right, metamath uses Reverse Polish Notation

>

> > > 7 , 3 +

> > > -------

> > > 10

>

> > > and you guessed it - UNIFY() to do the matching.

>

> > > ...

>

> > > RPN is equivalent to

>

> > > A & B -> C

>

> > > that is why my Inference Rules

> > > (and PROLOG CLAUSES themselves)

>

> > > are of this form:

>

> > > OR

>

> > > if( and(X , Y ), or(X,Y) ).

> > > if( and(not(X) , not(Y) ), not(or(X,Y)) ).

> > > if( and(not(X) , Y ), or(X,Y) ).

> > > if( and(X , not(Y) ), or(X,Y) ).

>

> > > TRANSITIVE IMPLICATION

>

> > > if( and(if(A,B) , if(B,C)), if(A,C) ).

>

> > > TRANSIVITIVE LESS THAN

>

> > > if( and(less(X,Y) , less(Y,Z)) , less(X,Z) ).

>

> > > etc. etc. Similar to Metamath RPN format and PROLOG CLAUSE format,

> > > same matching technique too.

>

> > > But the advantage of using PROLOG is it is built for BACKWARD

> > > CHAINING.

>

> > > MetaMath and DCProof are 'Natural Deduction' Logics - the Human writes

> > > the proof!

>

> > I'm not sure what all that means or how it is relevant, but why don't

> > we just try that simple theorem again: {(x,y) | x in S, y=x} is a

> > function mapping the set S onto itself -- not just some particular set

> > of names or whatever, but ANY set S, be it finite, infinite or empty.

> > It's true in every case. Run it through your program and post the

> > automatically generated proof here -- one without any quantifiers

> > whatsoever.

>

> > While you are at it, let's see its proof of the non-existence of {x |

> > ~x in x} and {x | x=x}.

>

> > What? It'll be a few more weeks? Take your time, Herc.

>

> > Dan

> > Download my DC Proof 2.0 software athttp://www.dcproof.com

>

> Well I just had a Glitch with the proof by contradiction!

>

> **********LOGIC21.PRO************

>

> CARTESIAN JOIN OF PROLOG LOGIC FACTS

>

> and(X,Y) :- t(X), t(Y).

> and(X,not(Y)) :- t(X), not(Y).

> not(and(X,Y)) :- not(X), not(Y).

>

> LEVEL 1 THEOREMS

> thrm(and(X,Y),1) :- and(X,Y).

> thrm(e(A,B),1) :- e(A,B).

>

> MODUS PONENS

> thrm(R,s(X)) :- thrm(L,X), if(L,R).

>

> PROOF BY CONTRADICTION

> thrm(L,s(X)) :- thrm(R,X), if(not(L),not(R)).

> thrm(not(L),s(X)) :- thrm(R,X), if(L,not(R)).

>

> SET OF SELF CONTAINED SETS sc

> if( e(X,X) , e(X,sc) ).

>

> RUSSELLS SET rs

> if( not(e(X,X)) , e(X,rs) ).

> if( e(X,rs) , not(e(X,X)) ).

>

> DATA

> e( ideas, abstract ).

> e( abstract, abstract ).

>

> e( dog, animals ).

> e( cat, animals ).

>

Note that in PROLOG, the arguments are reversible. An annoying

feature!

> ************************

>

> This is how to prove a contradiction.

>

> thrm(not(L),s(X)) :- thrm(R,X), if(L,not(R)).

>

> not(L) is a theorem

> when R is a (lower level) theorem

> and L->not(R)

>

> i.e. assume L, prove R&~R

> --> not(L)

>

> ****** TEST RUSSELL SET PROOF *****

>

> @ log21.

> ?- thrm( e(X,sc) , s(1) ).

> X = abstract

>

> OK - the formal system worked out

> abstract = { abstract , ... }

>

Of course. The constant "abstract" is the only one you declared to be

an "element" of itself.

> so

> selfcontained = { abstract , .. }

>

> ------------------------

>

> ?- thrm( e(X,rs) , s(1) ).

> NO

>

> OK - Prolog said e(X,rs) has no results

> i.e. Russell's set is at most empty.

>

> -------------------------

>

> ?- thrm( not(e(X,rs)), s(1) ).

> X = abstract

>

> ^^^^^^^^^^^^^^^

>

> WHAT? I tried to prove RUSSELL'S SET DOESN'T EXIST

>

> not(e(X,rs))

>

> and Prolog told me a Set that is NOT in RUSSELL'S SET!!!

>

> Haha! cracked me up... back to the drawing board...

>

> An alternative to NEGATION AS FAILURE??

>

> not(e(X,set)) ?

>

Good luck!

Dan

Download my DC Proof 2.0 software at http://www.dcproof.com