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,253
Registered: 5/20/10
Re: PREDICATE CALCULUS 2
Posted: Nov 27, 2012 6:58 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Nov 28, 8:41 am, 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).
>
> Dan
> Download my DC Proof 2.0 software athttp://www.dcproof.com
>



So what do you use?

EXIST( d, r1, r2 )
(d,r1) e S
(d,r2) e S
r1=/=r2

means a duplicate value in the 1st ordinate.

--------------------------

proposed( tom, jane )
proposed( mark, sally)
proposed( josh, sally )
proposed( henry, barb )

relation(proposed, MAN, WOMAN) <- proposed(MAN,WOMAN)

isfunction( R ) <- ALL(Y) relation( R, X1, Y ) , relation( R, X2,
Y ) , X1=X2

So I would have to convert the ALL(Y) to the Formal Prolog equivalent.

all( Y , d(Y) , p(Y) )

where

{ Y | d(Y) } C { Y | p(Y) }

----------------------------

Subset is then worked out using pure Unify and Recursion.



PROLOG+ A CONCEPT DATABASE MANAGEMENT LANGUAGE (DBML)

We add simple breadth first extensions to PROLOG CLAUSES.

Y> next record
Y< prev record
Y>> last record
Y<< 1st record

AXIOM OF FINITE SUBSETS
-----------------------

subs(A,X,Y) <- e(A>>,X) ^ e(A,Y).

subs(A,X,Y) <- e(A,Y) ^ e(A>,X) ^ subs(A,X,Y).

ss(X,Y) <- e(A<<,X) ^ subs(A,X,Y).


-----------

This is a FOR LOOP that goes through every result in a Database Table/
Query to calculate whether a Subset Relation exists.


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

So your question boils down to whether:

isfunction( R ) <- ALL(Y) relation( R, X1, Y ) , relation( R, X2,
Y ) , X1=X2

is expressible using only SUBSET and not ALL().

{ Y | d(Y) } C { Y | p(Y) }

-------------

It should work with something like...

{ Y | R(X1,Y) ^ R(X2,Y) } C {Y | R(X1,Y) ^ R(X2,Y) ^ X1=X2 }

No Quantifiers Needed!
Just Subset for ALL() and Double Variable Instantiation for EXIST()
and ANY()

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.