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 9:38 AM

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 at http://www.dcproof.com

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