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 ]
 Graham Cooper Posts: 4,495 Registered: 5/20/10
Re: PREDICATE CALCULUS 2
Posted: Nov 28, 2012 1:35 AM

On Nov 28, 2:26 pm, Dan Christensen <Dan_Christen...@sympatico.ca>
wrote:
> On Nov 27, 8:59 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
>

> > There are 2 ALLs which is more complicated but you can format it as a
> > SUBSET using a cartesian product of the 2 X values with a common Y.

>
> > isfunction(r)  <-  ALL(Y1) ALL(Y2) r(X,Y1)^r(X,Y2) -> Y1=Y2
>
> There is more to functionality than this. I may not fully understand
> your unusual notation (PROLOG?), but it would seem you have left out
> the requirement that FOR ALL elements of some domain set, THERE EXISTS
> a unique image in a codomain set. (This is where I think quantifiers
> become indispensable).
>

> > {(Y1,Y2)|r(X,Y1)^r(X,Y2)} C {(Y1,Y2)|r(X,Y1)^r(X,Y2)->Y1=Y2}
>
> [snip]
>
> The same comment applies... I think.
>
> Anyway, I am still waiting for proofs of the following:
>
> 1. {(x,y) | x in S, y=x}  is a function mapping the set S onto itself
> 2. {x | ~x in x} cannot exist
> 3. {x | x=x} cannot exist
>
> You really need to address these fundamental results.
>
> For what it is worth, and from what little I know about PROLOG, it
> doesn't seem to be capable of all that is required to do mathematical
> proofs in general. It may be able to model some interesting and useful
> aspects of predicate logic and set theory, but, for your purposes,
> important pieces of the puzzle seem to be missing.
>
> Dan
>

Nope, this is exactly the definition of function.

{(Y1,Y2) | r(X,Y1)^r(X,Y2)} C {(Y,Y) | r(X,Y)}

which simply guarantees only 1 Y value for any X value.

e.g.

----r------X1---X2
kiss( jane, tom )
kiss( sally, mark)
kiss( sally, josh )
kiss( barb, henry )

{ (Y1,Y2) | r(X,Y1)^r(X,Y2) }

= {
(tom,tom) *** X= jane
(mark,mark) *** X = sally
(josh,josh) *** X = sally
(mark,josh) *** X = sally
(josh,mark) *** X = sally
(henry,henry) *** X = barb
}

This is the GENERAL DOMAIN of ALL()

which must be a SUBSET of the SPECIFIED PREDICATE of ALL().

In this case the SUPERSET is smaller so the C relation is false and
the equivalent ALL() statement is false and the relation is not a
function.

ALL(term) domain(term) -> predicate(term)
/\
||
\/
{ term | domain(term) } C { term | predicate(term) }

Worked perfectly on the arbitrary formula you keep insisting it
doesn't work on!

DEFN OF FUNCTION - NO QUANTIFIERS
{(Y1,Y2) | r(X,Y1)^r(X,Y2)} C {(Y,Y) | r(X,Y)}

Herc

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