🚀 go-pugleaf

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
]
]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) '='?

The symbol '=' alone does not point out what variable is being
defined, but ':=', (which is defined formally by its usage) does.  I
did not discuss the rules for introducing X := E because they seemed
uninteresting.  It is clear that you need syntactic rules to avoid
naming conflicts and that rules must cover a range of clauses in a
proof.  That is, a definition has a scope that includes more than just
the clause in which it is introduced.  Clearly, no axiom or normal
rule of inference is adequate to specify this.

]... 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.  Non-creative, eliminable definitions are
no more than abbreviations, and mathematics cannot be done with such a
sparse notion of definition.
-- 
					David Gudeman
gudeman@cs.arizona.edu