home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2169 < prev    next >
Encoding:
Text File  |  1992-11-24  |  2.0 KB  |  43 lines
  1. Newsgroups: sci.logic
  2. Path: sparky!uunet!secapl!Cookie!frank
  3. From: frank@Cookie.secapl.com (Frank Adams)
  4. Subject: Re: recursive definitions and paradoxes
  5. Message-ID: <1992Nov23.195809.45768@Cookie.secapl.com>
  6. Date: Mon, 23 Nov 1992 19:58:09 GMT
  7. References: <26841@optima.cs.arizona.edu>
  8. Organization: Security APL, Inc.
  9. Lines: 32
  10.  
  11. In article <26841@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
  12. >In article  <BxzG21.Gnr@unx.sas.com> Gary Merrill writes:
  13. >]In article <26788@optima.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes:
  14. >]|> I propose for discussion the
  15. >]|> 
  16. >]|>   Axiom of Definition: (X := E /\ Exist! X.X=E) => X = E
  17. >]|> 
  18. >]|> where "Exist! x" means "there exists a unique x such that".  What if you
  19. >]
  20. >]... Definitions must
  21. >]satisfy such criteria as non-creativity (you can't prove something
  22. >][in "old" notation] by using the definition that you couldn't
  23. >]without it) and eliminability (the defined notation must be eliminable
  24. >]in *all* contexts).  The fact that the above axiom is being suggested
  25. >]seems to imply that the proposed "definition" does not satisfy the
  26. >]criterion of eliminability...
  27. >
  28. >Exactly.  Actually, my notion of definition does not satisfy either of
  29. >the two notions you mention.  Recursive definitions are creative and
  30. >non-eliminable, and for that reason they have to be protected with an
  31. >axiom that limits their use.
  32.  
  33. This statement is at best misleading.  The proposed notion of definition,
  34. with the axiom given, *is* eliminable (and hence non-creative), as I have
  35. noted in another posting.  *Without* the axiom given, it is of course also
  36. eliminable -- you can prove something about X given X := E iff you can
  37. prove it about a free variable X.  Only with the naive axiom of definition
  38. is it not eliminable -- and then it is inconsistent.
  39.  
  40. There are other axioms which could be added which would make this kind of
  41. definition non-eliminable, and David may have some such in mind.  No such
  42. have been presented, however.
  43.