The Math Forum

Search All of the Math Forum:

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

Math Forum » Discussions » sci.math.* » sci.math

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

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 ]
Dan Christensen

Posts: 8,219
Registered: 7/9/08
Posted: Nov 27, 2012 11:26 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Nov 27, 8:59 pm, Graham Cooper <> 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}


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.

Download my DC Proof 2.0 software at

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© The Math Forum at NCTM 1994-2018. All Rights Reserved.