Proof
For any proposition, we can build the sets
and
These are sets, using the axiom of specification. In classical set theory this would be equivalent to
and similarly for . 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).
Assuming the axiom of choice, there exists a choice function for the set ; that is, a function such that
By the definition of the two sets, this means that
- ,
which implies
But since (by the axiom of extensionality), therefore, so
Thus 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 theories with only the predicative separation, 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.
Read more about this topic: Diaconescu's Theorem
Famous quotes containing the word proof:
“If any doubt has arisen as to me, my country [Virginia] will have my political creed in the form of a “Declaration &c.” which I was lately directed to draw. This will give decisive proof that my own sentiment concurred with the vote they instructed us to give.”
—Thomas Jefferson (1743–1826)
“To cease to admire is a proof of deterioration.”
—Charles Horton Cooley (1864–1929)
“The source of Pyrrhonism comes from failing to distinguish between a demonstration, a proof and a probability. A demonstration supposes that the contradictory idea is impossible; a proof of fact is where all the reasons lead to belief, without there being any pretext for doubt; a probability is where the reasons for belief are stronger than those for doubting.”
—Andrew Michael Ramsay (1686–1743)