Diaconescu–Goodman–Myhill theorem

In mathematical logic, Diaconescu's theorem, or the Goodman–Myhill theorem, states that the full axiom of choice is sufficient to derive the law of the excluded middle, or restricted forms of it, in constructive set theory. It was discovered in 1975 by Diaconescu[1] and later by Goodman and Myhill[2].

For any proposition P\,, we can build the sets

U = \{x \in \{0, 1\} : (x = 0) \vee P\}, V = \{x \in \{0, 1\} : (x = 1) \vee P\}.

These are sets, using the axiom of specification. In classical set theory this would be equivalent to

U = \begin{cases} \{0,1\}, & \mbox{if } P \\ \{0\}, & \mbox{if } \neg P\end{cases}

and similarly for V\,. However, without the law of the excluded middle, these equivalences cannot be proven; in fact the two sets are not even provably finite (in the usual sense of being in bijection with a natural number, though they would be in the Dedekind sense).

By the axiom of choice, there will exist a choice function f\, for the set \{U, V\}\,; that is, a function f\, such that

[f(U) \in U] \wedge [f(V) \in V].\,

By the definition of the two sets, this means that

[(f(U) = 0) \vee P] \wedge [(f(V) = 1) \vee P]\,,

which implies f(U) \neq f(V) \vee P.

But since P \to (U = V), (by the axiom of extensionality),

therefore P \to (f(U) = f(V))\,,

so (f(U) \neq f(V)) \to \neg P.

Thus \neg P \vee P. As this could be done for any proposition, this completes the proof that the axiom of choice implies the law of the excluded middle.

The proof relies on the use of the full separation axiom. In constructive set theory usually only predicative separation is permitted. Thus the form of P will be restricted to sentences with bound quantifiers only, giving only a restricted form of the law of the excluded middle. This restricted form is still not acceptable constructively.

In constructive type theory, or in Heyting arithmetic extended with finite types, there is typically no separation at all - subsets of a type are given different treatments. A form of the axiom of choice is a theorem, yet excluded middle is not.

See also

  • Constructive choice principle

Notes

  1. ^ R. Diaconescu, "Axiom of choice and complementation", Proceedings of the American Mathematical Society 51:176-178 (1975)
  2. ^ N. D. Goodman and J. Myhill, “Choice Implies Excluded Middle”, Zeitschrift fur Mathematische Logik und Grundlaaen der Mathematik 24:461 (1975)

Open source encyclopedia content modification information:

This page was last modified on 17 July 2009 at 21:24.

Authorship and Review

Open source encyclopedia content provided here is not reviewed directly by MedLibrary.org. Content is sourced directly from Wikipedia and is authored by an open community of volunteers. It is not produced by or in any way affiliated with MedLibrary.org.

Usage Guidelines

This article is licensed under the GNU Free Documentation License. It uses material from the Wikipedia article on "Diaconescu–Goodman–Myhill theorem", which is available in its original form here:

http://en.wikipedia.org/w/index.php?title=Diaconescu%E2%80%93Goodman%E2%80%93Myhill_theorem

All material adapted used from Wikipedia is available under the terms of the GNU Free Documentation License. Wikipedia® itself is a registered trademark of the Wikimedia Foundation, Inc.