home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2163 < prev    next >
Encoding:
Text File  |  1992-11-23  |  1.8 KB  |  44 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.163357.52070@Cookie.secapl.com>
  6. Date: Mon, 23 Nov 1992 16:33:57 GMT
  7. References: <26922@optima.cs.arizona.edu>
  8. Organization: Security APL, Inc.
  9. Lines: 33
  10.  
  11. In article <26922@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
  12. >In article  <1992Nov21.230530.117800@Cookie.secapl.com> Frank Adams 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".
  19. >]
  20. >]Actually, no.  Unless I am much mistaken, this kind of definition is
  21. >]eliminable.  If we have a definition X := E, we can rewrite a wff of
  22. >]the form P(X) as (All X.((Ex! X.X=E) => X=E) => P(X)).
  23. >
  24. >I'm not sure what you mean.  If you mean that the definition plus the
  25. >axiom is eliminable, then of course you are right.
  26.  
  27. (I am leaving out the discussion of exactly how to eliminate the definition;
  28. it suffices that we agree it is eliminable.)
  29.  
  30. In my previous article, I quoted:
  31. >  And by adding some of the well-known machinery
  32. >from recursion theory to prove Exist!... you could also talk about a lot
  33. >of self-containing sets.  Wouldn't this theory be much more powerful
  34. >than ZF?
  35.  
  36. Perhaps I misunderstood; I though David was asserting that his definitions
  37. and axiom thereof would make a theory much more powerful than ZF.  If they
  38. are eliminable, they don't.
  39.  
  40. So I must have misinterpreted "the well-known machinery from recursion
  41. theory".  I think I know recursion theory fairly well, and I don't know just
  42. what is being referred to here.  Thus I have to ask David to explicate just
  43. exactly what machinery he wishes to import.
  44.