Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: PREDICATE CALCULUS 2
Replies: 23   Last Post: Nov 29, 2012 1:13 AM

 Messages: [ Previous | Next ]
 Dan Christensen Posts: 86 Registered: 4/13/07
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

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

Date Subject Author
11/25/12 Graham Cooper
11/27/12 Dan Christensen
11/27/12 Graham Cooper
11/27/12 Dan Christensen
11/27/12 Dan Christensen
11/27/12 Dan Christensen
11/27/12 Graham Cooper
11/27/12 Graham Cooper
11/27/12 Graham Cooper
11/27/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Virgil
11/28/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Dan Christensen
11/29/12 Graham Cooper
11/29/12 Dan Christensen
11/28/12 Frederick Williams
11/28/12 Dan Christensen
11/28/12 Dan Christensen