
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.
rX1X2 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

