|
|
Re: PREDICATE CALCULUS 2
Posted:
Nov 27, 2012 6:45 PM
|
|
On Nov 27, 6:42 pm, Dan Christensen <d...@dcproof.com> wrote:
> On Nov 27, 5:41 pm, Dan Christensen <d...@dcproof.com> wrote:
>
>
>
>
>
>
>
>
>
> > 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).
>
> Example: How will you formally prove that {(x,y) | x in S & y=x} is a
> function mapping S to itself?
>
> And how will you prove there cannot exist a set {x | ~x in x}?
>
And that there cannot exist a set {x | x=x}
Dan
Download my DC Proof 2.0 software at http://www.dcproof.com
|
|
