Search All of the Math Forum:

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

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

 Messages: [ Previous | Next ]
 Dan Christensen Posts: 8,161 Registered: 7/9/08
Re: PREDICATE CALCULUS 2
Posted: Nov 27, 2012 11:26 PM

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

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