ZF Set Theory and Law of the Excluded Middle

Solution 1:

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.