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