
Re: PREDICATE CALCULUS 2
Posted:
Nov 29, 2012 12:00 AM


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 nonexistence 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 ).
************************
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 , ... }
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)) ?
Herc

