🚀 go-pugleaf

In article <26841@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>In article  <BxzG21.Gnr@unx.sas.com> Gary Merrill writes:
>]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
>]
>]... 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...
>
>Exactly.  Actually, my notion of definition does not satisfy either of
>the two notions you mention.  Recursive definitions are creative and
>non-eliminable, and for that reason they have to be protected with an
>axiom that limits their use.

This statement is at best misleading.  The proposed notion of definition,
with the axiom given, *is* eliminable (and hence non-creative), as I have
noted in another posting.  *Without* the axiom given, it is of course also
eliminable -- you can prove something about X given X := E iff you can
prove it about a free variable X.  Only with the naive axiom of definition
is it not eliminable -- and then it is inconsistent.

There are other axioms which could be added which would make this kind of
definition non-eliminable, and David may have some such in mind.  No such
have been presented, however.