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: 86
Registered: 4/13/07
Re: PREDICATE CALCULUS 2
Posted: Nov 27, 2012 5:41 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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



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.