🚀 go-pugleaf

In article <1emo86INN4de@roche.csl.sri.com>, rar@csl.sri.com (Bob Riemenschneider) writes:
|> In article <By174J.JBM@unx.sas.com> sasghm@theseus.unx.sas.com (Gary Merrill) writes:
|> 
|>    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?).  ...
|> 
|> Beth's theorem ("Padoa's method is general"), a more-or-less immediate
|> consequence of the Craig interpolation lemma.  (No doubt Mr. Gudeman
|> will be unimpressed, however.)
|> 
|>                                                         -- rar

Also, apparently the general technique of converting recursive definitons
to explicit definitions is provided by Frege.  There is an old paper
of Quine's ("Tarski's Theory of Truth", reprinted in _Selected Logic
Papers_) in which he demonstrates a theory containing a "recursive
definition" that cannot be eliminated without rendering the theory
inconsistent.  However, since the extended theory contains the protosyntax
of the base theory, it is not clear what can be made of this for
claims about eliminability or uneliminability in general.
-- 
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