home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2157 < prev    next >
Encoding:
Internet Message Format  |  1992-11-23  |  2.4 KB
  1. Path: sparky!uunet!cs.utexas.edu!zaphod.mps.ohio-state.edu!uwm.edu!rutgers!concert!sas!mozart.unx.sas.com!sasghm
  2. From: sasghm@theseus.unx.sas.com (Gary Merrill)
  3. Newsgroups: sci.logic
  4. Subject: Re: recursive definitions and paradoxes
  5. Message-ID: <By6EvJ.EJ1@unx.sas.com>
  6. Date: 23 Nov 92 15:54:54 GMT
  7. References: <26841@optima.cs.arizona.edu> <By174J.JBM@unx.sas.com> <1emo86INN4de@roche.csl.sri.com>
  8. Sender: news@unx.sas.com (Noter of Newsworthy Events)
  9. Organization: SAS Institute Inc.
  10. Lines: 35
  11. Originator: sasghm@theseus.unx.sas.com
  12. Nntp-Posting-Host: theseus.unx.sas.com
  13.  
  14.  
  15. In article <1emo86INN4de@roche.csl.sri.com>, rar@csl.sri.com (Bob Riemenschneider) writes:
  16. |> In article <By174J.JBM@unx.sas.com> sasghm@theseus.unx.sas.com (Gary Merrill) writes:
  17. |> 
  18. |>    In article <26841@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
  19. |>    |> 
  20. |>    |> Exactly.  Actually, my notion of definition does not satisfy either of
  21. |>    |> the two notions you mention.  Recursive definitions are creative and
  22. |>    |> non-eliminable, and for that reason they have to be protected with an
  23. |>    |> axiom that limits their use.  Non-creative, eliminable definitions are
  24. |>    |> no more than abbreviations, and mathematics cannot be done with such a
  25. |>    |> sparse notion of definition.
  26. |> 
  27. |>    I have a vague recollection of a result that any recursive definition
  28. |>    is eliminable in favor of an explicit definition (Scott? Montague?  A faulty
  29. |>    memory?).  ...
  30. |> 
  31. |> Beth's theorem ("Padoa's method is general"), a more-or-less immediate
  32. |> consequence of the Craig interpolation lemma.  (No doubt Mr. Gudeman
  33. |> will be unimpressed, however.)
  34. |> 
  35. |>                                                         -- rar
  36.  
  37. Also, apparently the general technique of converting recursive definitons
  38. to explicit definitions is provided by Frege.  There is an old paper
  39. of Quine's ("Tarski's Theory of Truth", reprinted in _Selected Logic
  40. Papers_) in which he demonstrates a theory containing a "recursive
  41. definition" that cannot be eliminated without rendering the theory
  42. inconsistent.  However, since the extended theory contains the protosyntax
  43. of the base theory, it is not clear what can be made of this for
  44. claims about eliminability or uneliminability in general.
  45. -- 
  46. Gary H. Merrill  [Principal Systems Developer, C Compiler Development]
  47. SAS Institute Inc. / SAS Campus Dr. / Cary, NC  27513 / (919) 677-8000
  48. sasghm@theseus.unx.sas.com ... !mcnc!sas!sasghm
  49.