Suppose that we take constructive set theory and add the axiom $\forall x \forall y\ (x \in y) \lor \lnot (x \in y)$. Does this imply excluded middle, or are there still some formulas $\varphi$ for which $\varphi \lor \lnot \varphi$ isn't provable using this new axiom?



Does $\forall x \forall y\ (x \in y) \lor \lnot (x \in y)$ imply excluded middle?
It depends how much separation is available. If you can construct the set $\{ z \in \{ \emptyset \} \;|\; \varphi \}$ then you can show $\varphi \vee \neg \varphi$. So for theories with full separation, like IZF, you can derive excluded middle, whereas for CZF where you only have separation for bounded formulas, you can only get excluded middle for bounded formulas.


Edit: See Rathjen, [Indefiniteness in semi-intuitionistic set theories: On a conjecture of Feferman](https://www1.maths.leeds.ac.uk/%7Erathjen/Indefinite.pdf) for a set theory with bounded excluded middle, but in which $\mathbf{CH} \vee \neg \mathbf{CH}$ is unprovable.


