8
$\begingroup$

I know that the law of the excluded middle is implied in ZFC set theory, since it is implied by the axiom of choice. Taking away the axiom of choice, does ZF set theory (with axioms as stated in the corresponding Wikipedia article), imply the law of the excluded middle [for infinite sets]?

If you know of a proof to the answer to my question, could you please point me to it? If LEM does follow from ZF and you don't know the proof, do you know which axioms of ZF it follows from?

Thanks very much.

$\endgroup$
3
  • 5
    $\begingroup$ What do you mean by the law of excluded middle? It's usual to take it to be the schema $\phi\vee\neg \phi$. That follows from the underlying logic and has nothing specifically to do with set theory. $\endgroup$
    – user104955
    Oct 12, 2014 at 18:18
  • 13
    $\begingroup$ $\mathsf{ZF}$ is a theory in classical first order logic, and this logic proves the law of excluded middle. If you want your logic to be intuitionistic, there are two standard versions of set theory that one studies, $\mathsf{IZF}$ and $\mathsf{CZF}$. Neither proves excluded middle, and adding excluded middle to either recovers classical $\mathsf{ZF}$. A good reference is here. $\endgroup$
    – Andrés E. Caicedo
    Oct 12, 2014 at 18:20
  • 3
    $\begingroup$ A slight re-pharasing of the previous comments (which are correct) to answer literally the question of which ZF-axioms are used to obtain the law of the excluded middle: No ZF-axioms are used, because the law of the excluded middle is part of the logic on which ZF is based. $\endgroup$
    – Andreas Blass
    Oct 12, 2014 at 18:53

1 Answer 1

Reset to default
4
$\begingroup$

Thanks for the responses GME, Andres, and Andreas. I think my question is answered. (GME I do indeed mean $\phi \vee \neg \phi $).

Let me make sure I understand your answers...

We have logic axioms and set theory axioms. ZF is set theory axioms consistent with the axioms for first-order logic, which is already not intuitionistic since LEM is included in those axioms. So, ZF is not intuitionistic.

If we want a "version" of ZF that is intuitionistic, we have to adjust the logic axioms by removing LEM, and then we will have to adjust the set theory axioms to be consistent with the new logic we are building it on. We will still try to make these new axioms resemble ZF as much as possible. So, take first-order logic, remove LEM, then adjust ZF, and we can get something like IZF or CZF.

What if we want to add the axiom of choice to IZF or CZF? My guess would be that this is exactly equivalent to adding AC to ZF (unless adjusting the set theory axioms as described in the previous paragraph results in some unforeseen consequences) - since AC implies LEM, by adding AC to IZF or CZF we "complete" our weakened first-order logic to once again have LEM, so that IZF/CZF is now ZF again, but with AC it is actually ZFC. (So, by adding AC to IZF/CZF, we lose the entire point of originally constructing IZF/CZF, since we end up at a non-intuitionistic theory again).

Basically, in my question I was assuming that ZF was built on a logic that didn't include LEM. This assumption was false, so my question is moot.

Does this all seem correct?

Thanks again.

$\endgroup$
5
  • $\begingroup$ By the way I know I can check answers on this site as a way of saying thanks, but how do I do the equivalent for your comments on my question? $\endgroup$
    – user3558855
    Oct 12, 2014 at 19:04
  • $\begingroup$ Leaving aside the part about LEM being part of the underlying logic, how does it follow from AC? $\endgroup$
    – bof
    Oct 12, 2014 at 19:13
  • 3
    $\begingroup$ Before posting this question I was jumping around the Internet looking for an answer, and quickly ran into Diaconescu's theorem, which says that LEM follows from AC. Here is a link: en.wikipedia.org/wiki/Diaconescu's_theorem. $\endgroup$
    – user3558855
    Oct 12, 2014 at 19:19
  • $\begingroup$ @bof - see Set Theory: Constructive and Intuitionistic ZF : CZF + EM = ZF and for Choice : "the assumption of the axiom of choice gives rise to instances of the excluded middle in extensional contexts, where a form of separation is also available. This is the case for example of constructive and intuitionistic ZF." $\endgroup$
    – Mauro ALLEGRANZA
    Oct 12, 2014 at 20:09
  • 1
    $\begingroup$ I don't know about AC in IZF and CZF, but everything else you say is correct. $\endgroup$
    – user104955
    Oct 12, 2014 at 21:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .