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 ]
Graham Cooper

Posts: 4,267
Registered: 5/20/10
Re: PREDICATE CALCULUS 2
Posted: Nov 29, 2012 12:00 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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

************************

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



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.