Date: Nov 28, 2012 5:42 PM
Author: Dan Christensen
Subject: Re: PREDICATE CALCULUS 2

On Nov 28, 4:45 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> 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 you 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}.

>
> 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 )
>


Actually, you will need at least a 3 parameter predicate -- another
one for the codomain, possibly more for functions of more than 1
variable.


> it's also do-able, but I have no idea what purpose isFunctionOf would
> have.
>


When the only tool you have is a hammer, every problem looks like a
nail.

You may want prove that a function is well-defined. You just can't do
that in PROLOG as far as I know. The simplest example is one I have
already given here:

To prove {(x,y) | x in S, y=x} is a function mapping the set S onto
itself. (See my Samples directory for my own formal proof.) There is
no way that this can be output from PROLOG in any form.


> PROLOG is just the UNIFY( f1(..) , f1(...) )
>


I would love to be proven wrong, but I don't think you will get very
far in abstract mathematics using only PROLOG. If you are still
determined to used PROLOG, you might look at Norm Megill's MetaMath
program -- the gold standard of mechanized rigour IMHO. It is very
small program and, as I understand, is based entirely on making
symbolic substitutions. Your "facts" would be facts about formuala's,
not individual objects. Just maybe you can implement it in PROLOG.
Write to Norm. He will be able to advise you. He probably knows PROLOG
as well.

Then, of course, there is, ahem... my own DC Proof program. If you
don't like the axioms I have built into it, you can use it to make up
your own. I will show you how if you need help.

Dan
Download my DC Proof 2.0 software at http://www.dcproof.com