The axiom of choice and the law of excluded middle in weak set theories
| Abstract | In constructive mathematics the axiom of choice (AC) has a somewhat ambiguous status. On the one hand, in intuitionistic set theory, or the local set theory associated with a topos ([2]) it can be shown to entail the law of excluded middle (LEM) ([ 3 ], [ 5 ]). On the other hand, under the “propositions-as types” interpretation which lies at the heart of constructive predicative type theories such as that of Martin-Löf [9], the axiom of choice is actually derivable (see, e.g. [11] ), and so certainly cannot entail the law of excluded middle. This incongruity has been the subject of a number of recent investigations, for example [6], [7], [9], [12]. What has emerged is that for the derivation of LEM from AC to go through it is sufficient that sets (in particular power sets), or functions, have a degree of extensionality which is, so to speak, built into the usual set theories but is incompatible with constructive type theories Another condition, independent of extensionality, ensuring that the derivation goes through is that any equivalence relation determines a quotient set. LEM can also be shown to follow from a suitably extensionalized version of AC. The arguments establishing these intriguing results have mostly been formulated within a type-theoretic framework. It is my purpose here to formulate and derive analogous results within a comparatively straightforward set-theoretic framework. The core principles of this framework form a theory – weak set theory WST – which lacks the axiom of extensionality1 and supports only minimal set-theoretic constructions. WST may be considered a fragment both of (intuitionistic) ∆0-Zermelo set theory and Aczel’s constructive set theory ([1]). In particular WST is, like constructive type theories, too weak to allow the derivation of LEM from AC. But we shall see that , as with constructive type theories, beefing up WST with extensionality principles (even very moderate ones) or quotient sets enables the derivation to go through.. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,701 |
| External links |
  Try with proxy. Try with proxy. |
| Through your library | Only published papers are available at libraries |
Similar books and articlesAdam Rieger (2000). An Argument for Finsler-Aczel Set Theory. Mind 109 (434):241-253.
Steve Awodey (2008). A Brief Introduction to Algebraic Set Theory. Bulletin of Symbolic Logic 14 (3):281-298.
Nicola Gambino & Peter Aczel (2006). The Generalised Type-Theoretic Interpretation of Constructive Set Theory. Journal of Symbolic Logic 71 (1):67 - 103.
J. L. Bell (1997). Zorn's Lemma and Complete Boolean Algebras in Intuitionistic Type Theories. Journal of Symbolic Logic 62 (4):1265-1279.
Bart Jacobs (1989). The Inconsistency of Higher Order Extensions of Martin-Löf's Type Theory. Journal of Philosophical Logic 18 (4):399 - 422.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads45 ( #24,555 of 549,125 )Recent downloads (6 months)4 ( #19,263 of 549,125 )How can I increase my downloads? |
My notes
Discussion
