🚀 go-pugleaf

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