🚀 go-pugleaf

In article <26788@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:

|> I propose for discussion the
|> 
|>   Axiom of Definition: (X := E /\ Exist! X.X=E) => X = E
|> 
|> where "Exist! x" means "there exists a unique x such that".  What if you

I have not *carefully* read the rest of this posting.  However, on
the face of it, it appears that this "axiom of definition" is quite
suspect.  I'm not sure what

	X := E

means.  If it is really intended to represent a *definition* of X,
then why is the new axiom necessary?  What exactly is the symbol
':=' meant to express beyond (or short of) '='?  If the
"Axiom of Definition" is being proposed for discussion, we really
need some more axioms for ':=', since at the moment it appears only
on the left-hand side of one conditional axiom and otherwise has
some informal semantics (it is said to be a "definition") attached
to it.  The standard approach, of course, is to introduce definitions
into theories by using the usual '=' and '<->'.

It is quite correct to observe that "we have to be careful what we
take to be a definition".  There is a fairly widely known *theory*
of definition in which certain criteria must be satisfied in order
for a formula to be a definition (actually, things are probably
better put in terms of "definitional extensions" of theories).
I can't put my hands on specific references at the moment, but the
names of Patrick Suppes and Quine come to mind.  Definitions must
satisfy such criteria as non-creativity (you can't prove something
[in "old" notation] by using the definition that you couldn't
without it) and eliminability (the defined notation must be eliminable
in *all* contexts).  The fact that the above axiom is being suggested
seems to imply that the proposed "definition" does not satisfy the
criterion of eliminability.  (Certain of the paradoxes failed in
the system of my dissertation because it could be shown that the
proposed "definition" of the truth predicate required did not
constitute a definitional extension of the theory.)

At any rate, it seems that any discussion should take place within
the context of the theory (or at least *a* theory, and then why
not the usual one?) of definition.
-- 
Gary H. Merrill  [Principal Systems Developer, C Compiler Development]
SAS Institute Inc. / SAS Campus Dr. / Cary, NC  27513 / (919) 677-8000
sasghm@theseus.unx.sas.com ... !mcnc!sas!sasghm