|
|
Re: PREDICATE CALCULUS 2
Posted:
Nov 27, 2012 5:41 PM
|
|
On Nov 27, 5:14 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> On Nov 28, 12:38 am, Dan Christensen <d...@dcproof.com> wrote:
>
>
>
>
>
>
>
>
>
> > On Nov 25, 10:36 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
>
> > > Predicate Calculus only uses the e(member,set)
> > > predicate to construct set theoretic formula.
>
> > > I convert ALL() Quantifiers to a SUBSET OF TERM Predicate
>
> > > all(X,d(..X..),p(..X..))
> > > /\
> > > ||
> > > \/
> > > {X|d(..X..)} C {X|p(..X..)}
>
> > > Either formula can be converted to High Order Prolog.
>
> > > HOP e.g.
>
> > > all( X , less(X,3) , add( X, {1,2,3,4}, 4) )
> > > ^ ^ DOMAIN SUPERSET
> > > | |
> > > | TERM
> > > |
> > > QUANTIFIER
>
> > > All(X):X<3 X+{1,2,3 or 4}=5
> > > /\
> > > || LOGIC FORMULA
> > > ||
> > > \/
> > > all( X , less(X,3) , add( X, {2,3,4}, 4) ) *HOP*
> > > /\
> > > ||
> > > || SET FORMULA
> > > \/
> > > { X | less(X,3) } C { X | add(X, {1,2,3,4}, 4) }
> > > |
> > > |
> > > | ELEMENTS
> > > \/
> > > {0,1,2} C {0,1,2,3}
> > > |
> > > v
> > > TRUE
>
> > > Herc
> > > --
> > > if( if(t(S),f(R)) , if(t(R),f(S)) ).
> > > if it's sunny then it's not raining
> > > ergo
> > > if it's raining then it's not sunny
>
> > In your proposed system, how do you determine whether or not a given
> > set of ordered pairs represents a function mapping one set to another?
> > (You will probably need existential quantifiers.)
>
> > Dan
> > Download my DC Proof 2.0 software athttp://www.dcproof.com
>
> Everything is Relational with multiple records for results.
>
> Using Charlie Boo's system.
>
> add( X, 0, 0 ).
> add( s(X), 0, s(Y) ) <- add( X, 0, Y ).
> ...
>
> This happens to be a function by it's effective definition.
>
> RELATION ADD
>
> m n a
> ________
> 0 0 0
> s(0) 0 s(0)
> s(s(0)) 0 s(s(0))
> ...
>
> where the BAR ____ means (m,n) tuples are unique.
>
> ...
>
> But Prolog doesn't have uniqueness constraints, entire rows can be
> duplicated and it's the same relation, like duplicating elements of a
> set. The POST-PARSER may format the results by removing duplicates of
> the final relation.
>
> There is nothing stopping you adding a fact
>
> ADD(1,2,4).
>
> Now (1,2) has 2 entries and is no longer a function.
>
> --------------------------
>
> 1st you have to recognise which ALL(x) are merely ANY(x)
>
> SUBSET 'C' is already defined.
>
> ...
>
> [PERSON]
>
> ALL(s1) ALL(s2) s1 C s2 ^ s2 C s1
> -> s1 = s2
>
> ...
>
> [PERSON PREPARSES HIS LOGIC FORMULA]
>
> ANY(s1) ANY(s2) s1 C s2 ^ s2 C s2
> -> s1= s2
>
> [FORMAL PROLOG PREPARSER]
> S1 C S2 ^ S2 C S1
> -> S1 = S2
>
> if( and( c(S1,S2) , c(S2,S1)) , =(S1,S2) ).
> FACT ADDED
>
> -------------------------
>
> It might look clumsy but
> if( and(..,..) , ... )
>
> is how most rules work, even the predicates themselves, by doing a
> cartesian join on pairs of theorems.
>
> I will do a new post on the if(and...)) system when I get proof by
> contradiction working, which is almost identical to just using modus
> ponens!
>
> MP
> t(R) <- if(L,R), t(L).
>
> MP Variation
> t(R) <- if(not(L),R), not(L).
>
> PROOF BY CONTRADICTION
> t(R) <- if(not(R),L), not(L).
>
> Herc
>
> --
> LOG20.PRO
>
> PREDICATE CONSTRUCTION
>
> 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) ).
>
> if( and(not(X) , not(Y) ), not(and(X,Y)) ).
> if( and(not(X) , Y ), not(and(X,Y)) ).
> if( and(X , not(Y) ), not(and(X,Y)) ).
>
> if( and(X , Y ), if(X,Y) ).
> if( and(not(X) , not(Y) ), if(X,Y) ).
> if( and(not(X) , Y ), if(X,Y) ).
> if( and(X , not(Y) ), not(if(X,Y)) ).
>
> if( and(X , Y ), iff(X,Y) ).
> if( and(not(X) , not(Y) ), iff(X,Y) ).
> if( and(not(X) , Y ), not(iff(X,Y)) ).
> if( and(X , not(Y) ), not(iff(X,Y)) ).
>
> ...
>
> TRANSITIVE RULES...
>
> if( and(if(A,B) , if(B,C)), if(A,C) ).
>
> if( not(not(X)) , X ).
> if( not(and(X,Y)) , or(not(X),not(Y)) ).
> if( not(or(X,Y)) , and(not(X),not(Y)) ).
>
> ...
>
> CARTESIAN JOIN OF THEOREMS
>
> and(X,Y) :- t(X), t(Y).
> and(X,not(Y)) :- t(X), not(Y).
> and(not(X),not(Y)) :- not(X), not(Y).
> and(not(X),Y) :- not(X), t(Y).
>
> t(and(X,Y)) :- and(X,Y).
>
> ...
>
> MODUS PONENS
>
> t(R) :- if(L,R), t(L).
>
> ...
>
> ARITHMETIC
>
> t(less(X,Y)) :- less(X,Y).
> less(0,X).
> if( and(less(X,Y) , less(Y,Z)) , less(X,Z) ).
>
> ...
>
> <NEXT WEEK IN FORMAL PROLOG - PROOF BY CONTRADICTION>
All very confusing, but it doesn't seem to answer my question. If I
describe a set of ordered pairs, how will you be able to tell whether
it represents a function mapping one particular set to another? It
would be interesting to see if you can do this without existential
quantifiers. If you have them, you also have universal quantifiers
(their negation).
Dan
Download my DC Proof 2.0 software at http://www.dcproof.com
|
|
