
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

