
Re: PREDICATE CALCULUS 2
Posted:
Nov 28, 2012 4:45 PM


On Nov 29, 6:32 am, Dan Christensen <Dan_Christen...@sympatico.ca> wrote: > On Nov 28, 2:41 pm, Graham Cooper <grahamcoop...@gmail.com> wrote: > > > > > > > > > > > On Nov 29, 1:13 am, Dan Christensen <Dan_Christen...@sympatico.ca> > > wrote: > > > > On Nov 28, 1:35 am, Graham Cooper <grahamcoop...@gmail.com> wrote: > > > > > 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. > > > > > 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. > > > > This is a common mistake. According to this erroneous view, every set > > > {(x,y)} is a function for any objects x and y. The functionality of a > > > set of ordered pairs is always defined in terms of a domain and > > > codomain set. Here is a typical formal(ish) definition of a function > > > from Wiki (my comments in []'s): > > > > "A function f from X [the domain of f] to Y [the codomain of f] is a > > > subset of the Cartesian product X × Y subject to the following > > > condition: every element of X is the first component of one and only > > > one ordered pair in the subset.[3] In other words, for every x in X > > > there is exactly one element y such that the ordered pair (x, y) is > > > contained in the subset defining the function f."http://en.wikipedia.org/wiki/Function_(mathematics)#Definition > > > > Example: Let X=Y={0,1}. > > > > Then {(0,0), (1,1)} is function from X to Y, while {(0,1)} is not. > > > Semantics escapes you! > > Just how are you going to implement the above definition of a function > in your formal system without universal and existential quantifiers? > You can't. > > This looks like a major setback for your project, Herc. If you want my > opinion  I can't imagine that your do  but nevertheless I really > don't think PROLOG is the way to go. It is not a theorem prover. It is > just another database query language. It doesn't do generalizations. > For that, you need quantifiers. > > > {(0,1)} is a function. > > You can say {(0,1)} is a function only if you also say that the domain > of that function is {0}. > > Dan > Download my DC Proof 2.0 software athttp://www.dcproof.com >
You 2 aren't making any sense.
I converted the Quantified Defn to a SUBSET defn.
If you want a 2 parameter predicate
isFunctionOf( r , d )
instead of isFunction( r )
it's also doable, but I have no idea what purpose isFunctionOf would have.
PROLOG is just the UNIFY( f1(..) , f1(...) )
You need it to match the parameters of the LHS of the inference rule, as it happens it's also computationally complete.
Herc

