home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2139 < prev    next >
Encoding:
Text File  |  1992-11-21  |  1.3 KB  |  33 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: <1992Nov21.230530.117800@Cookie.secapl.com>
  6. Date: Sat, 21 Nov 1992 23:05:30 GMT
  7. References: <26788@optima.cs.arizona.edu>
  8. Organization: Security APL, Inc.
  9. Lines: 22
  10.  
  11. In article <26788@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
  12. >I propose for discussion the
  13. >
  14. >  Axiom of Definition: (X := E /\ Exist! X.X=E) => X = E
  15. >
  16. >where "Exist! x" means "there exists a unique x such that".  What if you
  17. >altered ZF to contain this axiom (and introduction of definitions)?  In
  18. >the first place, you could immediately prove the existence of all sets
  19. >that are already there.  And by adding some of the well-known machinery
  20. >from recursion theory to prove Exist!... you could also talk about a lot
  21. >of self-containing sets.  Wouldn't this theory be much more powerful
  22. >than ZF?
  23.  
  24. Actually, no.  Unless I am much mistaken, this kind of definition is
  25. eliminable.  If we have a definition X := E, we can rewrite a wff of
  26. the form P(X) as (All X.((Ex! X.X=E) => X=E) => P(X)).
  27.  
  28. (This rewrite is a bit complicated, since it covers the case where X is not
  29. uniquely defined.  The essential form is (All X.X=E => P(X)), which can be
  30. used if Ex! X.X=E has been proved.)
  31.  
  32. Please try again.
  33.