|
|
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
|
|
