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?

3$\begingroup$ You are confounding excluded middle with "there is a formula $\phi$ such that neither $\phi$ nor $\lnot \phi$ is provable". Even if we remove the faulty use of "provable" and consider "there is $\phi$ such that neither $\phi$ nor $\lnot \phi$", which is expressed as $\exists \phi . \lnot \phi \land \lnot\lnot \phi$, that is not excluded middle! It's an outright false statement (constructively and classically). $\endgroup$– Andrej BauerAug 2, 2020 at 17:49

$\begingroup$ Sorry, I wrote that without thinking. $\endgroup$– JamesAug 2, 2020 at 22:37

1$\begingroup$ No problem, I am just pointing it out so that you can edit the question, lest this sort of error spreads. I have seen experienced mathematicians make it (and conclude that constructive mathematics is nonsense). $\endgroup$– Andrej BauerAug 2, 2020 at 22:52

4$\begingroup$ If Feferman asked (a special case of) this question, and Rathjen researched it, and 11 people upvoted the answer, isn’t the question worth more than two upvotes? $\endgroup$– Matt F.Aug 3, 2020 at 3:06
2 Answers
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 semiintuitionistic set theories: On a conjecture of Feferman for a set theory with bounded excluded middle, but in which $\mathbf{CH} \vee \neg \mathbf{CH}$ is unprovable.

$\begingroup$ Does the end of your sentence ("you can only get excluded middle for bounded formulas") mean that, say, CZF + @James's axiom + $\lnot\text{EM}$ is consistent, or does it only mean that your trick for proving EM doesn't work? $\endgroup$– LSpiceAug 2, 2020 at 17:12

3$\begingroup$ As far as I can remember CZF with bounded excluded middle is strictly weaker than ZF, but I'll have to think a bit to find a proof or reference. $\endgroup$– awsAug 2, 2020 at 17:47

$\begingroup$ In CZF, if $\phi$ is “every set is in onetoone correspondence with some cardinal”, I doubt you can prove $\phi \vee \neg \phi$ from the proposed axiom. $\endgroup$– Matt F.Aug 2, 2020 at 17:54

$\begingroup$ I added a reference in an edit. @MattF. I agree, but I don't know a proof offhand. $\endgroup$– awsAug 2, 2020 at 20:02

1$\begingroup$ @aws We may refer Constructive ZermeloFraenkel Set Theory, Power Set, and the Calculus of Constructions by Rathjen. According to this article, $\mathsf{CZF}(\mathcal{P})$ with the bounded LEM (which is a subtheory of Tharp's quasiintuitionistic set theory) has the equal prooftheoretic strength of $\mathsf{KP}(\mathcal{P})$. Hence CZF with bounded LEM is weaker than ZF. $\endgroup$ Aug 2, 2020 at 20:22
This statement does imply excluded middle in a theory like IZF which has full separation. See https://us.metamath.org/ileuni/exmidel.html for a formalization of this in IZF. The notation there is that DECID $\phi$ is defined to be $\phi \vee ¬ \phi$ and EXMID is defined using a few technicalities but it implies $\psi \vee ¬ \psi$ for any proposition $\psi$.

2$\begingroup$ Isn’t your answer a proper subset of the other answer? $\endgroup$ Aug 13, 2022 at 18:45

$\begingroup$ I do also agree with that answer  my apologies if overlapping answers are frowned upon. $\endgroup$ Aug 13, 2022 at 19:33