Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math.independent

Topic: PREDICATE CALCULUS 2
Replies: 23   Last Post: Nov 29, 2012 1:13 AM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Dan Christensen

Posts: 2,428
Registered: 7/9/08
Re: PREDICATE CALCULUS 2
Posted: Nov 29, 2012 1:13 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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




Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.