|
Re: PREDICATE CALCULUS 2
Posted:
Nov 29, 2012 1:13 AM
|
|
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
|
|