🚀 go-pugleaf

In article <26841@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
|> 
|> 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.

I have a vague recollection of a result that any recursive definition
is eliminable in favor of an explicit definition (Scott? Montague?  A faulty
memory?).  At any rate, concerning the claim that mathematics cannot
be done with "such a sparse notion of definition", it is interesting
to inspect Chapters X and XI of Kalish and Montague where the theory
of commutataive ordered fields is definitionally extended to the theory
of real numbers which in turn is definitionally extended to the
theory of convergence.  A sketch is then given of how this can be
extended to the integral calculus (including an explicit definition
of the Riemann integral).  In passing, it is observed that the 'recursive
definition' of sigma (the summation operator) used in the theory can be
replaced by an explicit definition.  All this rests in part on the work
of Scott on arbitrary variabe binding operators.

Perhaps you really want to avoid talk of "definition" and simply speak
of "axiomatization".
-- 
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