home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / math / 15000 < prev    next >
Encoding:
Internet Message Format  |  1992-11-15  |  2.9 KB
  1. Path: sparky!uunet!europa.asd.contel.com!darwin.sura.net!jvnc.net!netnews.upenn.edu!sagi.wistar.upenn.edu
  2. From: weemba@sagi.wistar.upenn.edu (Matthew P Wiener)
  3. Newsgroups: sci.math
  4. Subject: Re: When's a proposition provable w/ choice indep. of choice?
  5. Keywords: Axiom of Choice, logic, set theory, intuitionism, constructionism, nonstandard analysis
  6. Message-ID: <97732@netnews.upenn.edu>
  7. Date: 15 Nov 92 18:50:27 GMT
  8. References: <1e3qvjINN3ul@iskut.ucs.ubc.ca>
  9. Sender: news@netnews.upenn.edu
  10. Reply-To: weemba@sagi.wistar.upenn.edu (Matthew P Wiener)
  11. Organization: The Wistar Institute of Anatomy and Biology
  12. Lines: 41
  13. Nntp-Posting-Host: sagi.wistar.upenn.edu
  14. In-reply-to: pruss@math.ubc.ca (Alexander Pruss)
  15.  
  16. In article <1e3qvjINN3ul@iskut.ucs.ubc.ca>, pruss@math (Alexander Pruss) writes:
  17. >       Are there any ways of judging whether a proposition is in some way
  18. >independent of the axiom of choice, without trying to prove/disprove it
  19. >without Choice?  The application would be to take a proposition which is
  20. >proved with the axiom of choice, and be able to assert that it holds even
  21. >without the axiom of choice, without going through the proof.
  22.  
  23. Yes--it's a notion called "absoluteness".  The only case I've seen of
  24. the above was an invocation of model-theoretical results that depended
  25. on GCH, and the claim that the final result itself did not need it.
  26.  
  27. >[...]  A similar but stricter question is whether there is any guideline
  28. >for determining if a proposition of a certain form being provable in
  29. >ordinary set theory is thence constructively provable. [...]
  30.  
  31. The easy result, which you realized yourself, is that all first order
  32. statements about the positive integers are absolute.  (Meaning that
  33. all quantifiers are for integers.)  A step beyond is the realization
  34. that an existential second-order quantifier over sets of the integers
  35. preserves absoluteness upwards.  That is, given a purely first-order
  36. statement, quantified by "there exists a function f:N->N" or something
  37. like that, if its true in a small model, it will be true in a larger
  38. model.
  39.  
  40. The canonical choice of "small model" is Goedel's constructible universe
  41. L.  Since L models AC, anything proven in L that is absolute upward is
  42. true without assuming AC.  This kind of diagram chasing, where truth and
  43. not elements is what gets kicked around, bugs some people, so it's worth
  44. realizing that all that's done is the search for the quantifier witness
  45. is done via the time-honored method of looking for a particular kind of
  46. witness.  In this case, one that's part of a well-ordered universe.
  47.  
  48. Things get exciting though.  Shoenfield has an absoluteness theorem
  49. which state that the first non-obviosity here also works.  If you have
  50. a statement "there exists f, for all g,h <1o arithmetic>", then it too
  51. will be absolute between L and V.  So any use of choice is redundant
  52. for such a statement also.
  53.  
  54. See Jech SET THEORY for the precise statement and proof.
  55. -- 
  56. -Matthew P Wiener (weemba@sagi.wistar.upenn.edu)
  57.