|
|
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
Download my DC Proof 2.0 software at http://www.dcproof.com
|
|
