```Date: Nov 28, 2012 3:32 PM
Author: Dan Christensen
Subject: Re: PREDICATE CALCULUS 2

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 functionin your formal system without universal and existential quantifiers?You can't.This looks like a major setback for your project, Herc. If you want myopinion -- I can't imagine that your do -- but nevertheless I reallydon't think PROLOG is the way to go. It is not a theorem prover. It isjust 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 domainof that function is {0}.DanDownload my DC Proof 2.0 software at http://www.dcproof.com
```