# Are Regularity schema and $\in$-induction schema equivalent in intuitionistic logic?

the answer was that they are equivalent in classical first order logic with membership "$$\in$$".

But the answer relies on rule of excluded middle? hence the following question:

Question: Are Regularity (as presented in the above mentioned link) and $$\in$$-induction schemas equivalent in intuitionistic logic?

• This nLab article would seem to indicate no, they are not equivalent. Note also that regularity plus the existence of a non-empty set is enough to imply excluded middle. Nov 9, 2018 at 15:37
• There are several inequivalent non-classical set theories, which one do you mean? Nov 10, 2018 at 5:14

As discussed in the nLab link I posted in my comment, the existence of a non-trivial relation satisfying regularity implies the law of excluded middle. We can use this to show that regularity and $$\in$$-induction are not intuitionistically equivalent. I'll transcribe their proof into your context:

Assume that there are two elements $$a$$ and $$b$$ satisfying $$a\in b$$ and assume that $$\in$$ satisfies the regularity scheme. Let $$\varphi$$ be any sentence and define a formula $$\psi_\varphi(x)$$ given by $$x=b \vee \left( x \in b \wedge \varphi \right)$$. Since we have the regularity scheme this applies to the formula $$\psi_\varphi (x)$$, i.e. we have

$$\exists x\psi_\varphi(x) \rightarrow \exists x (\psi_\varphi (x)\wedge \lnot\exists z\in x(\psi_\varphi(z)))$$

Clearly we have that $$\psi_\varphi (b)$$ holds, so $$\exists x\psi_\varphi(x)$$ holds and by modus ponens $$\exists x (\psi_\varphi (x)\wedge \lnot\exists z\in x(\psi_\varphi(z)))$$ holds as well. Let $$c$$ be such that $$\psi_\varphi (c) \wedge \lnot \exists z\in c (\psi_\varphi(z))$$. Since $$\psi_\varphi (c)$$ holds we have two possibilities: Either $$c=b$$ or $$c \in b \wedge \varphi$$. Obviously in the second case $$\varphi$$ holds. In the first case we can show by contradiction (which is intuitionistically valid as long as we're proving a negative) that $$\neg \varphi$$ holds. Specifically, assume that $$\varphi$$ holds, then this would imply that $$a\in b \wedge \psi_\varphi (a)$$, which implies $$\exists z \in b (\psi_\varphi (z))$$ and hence $$\exists z \in c (\psi_\varphi (z))$$, contradicting the choice of $$c$$. Therefore in this case, $$\varphi \rightarrow \bot$$, or in other words, $$\neg \varphi$$. So by cases we have $$\varphi \vee \neg \varphi$$, i.e. the law of excluded middle holds for $$\varphi$$. Since $$\varphi$$ was arbitrary we have that it holds for every sentence.

Now to see the separation consider Heyting arithmetic and let $$<$$ take the role of your symbol $$\in$$. It's not hard to see that the induction scheme in Heyting arithmetic is literally $$\in$$-induction with $$<$$ taking the role of $$\in$$. It's well known that Heyting arithmetic does not prove the law of excluded middle for all sentences. On the other hand if we take Heyting arithmetic and replace the induction scheme with the regularity scheme, again with $$<$$ taking the role of $$\in$$, then by the argument above, using $$a=0$$ and $$b=1$$ we get that the law of excluded middle holds for every sentence, i.e. the system we get is Peano arithmetic, which of course is not intuitionistically equivalent to Heyting arithmetic.

Since we got that the regularity scheme and the $$\in$$-induction scheme are not logically equivalent in the presence of additional assumptions (i.e. the non-induction axioms of Heyting/Peano arithmetic), they cannot possibly be intuitionistically equivalent over any weaker set of assumptions, including no assumptions at all. So they are not intuitionistically equivalent.

• this shows that Regularity schema implies $\in$-induction, but the converse is not true, so the Regularity scheme is stronger than $\in$-induction schema, under intuitionistic logic. Nov 11, 2018 at 15:41

I just wanted to extend on the answer of James Hanson, that along his arguments, it is not only the case that $$\in$$-induction is strictly weaker than Regularity schema given the conditions of Heyting arthimetic or weaker grounds! Even if we hold all axioms of ZF-Regularity and add to it $$\in$$-induction [on top of intuitionistic first order set language], still the resultant system is a strict subtheory of the theory resulting from adding Regularity schema, instead of $$\in$$-induction, while keeping the rest of axioms. The reason is because intuitionistic ZF doesn't prove the law of excluded middle, while if Regularity is added then this would enforce excluded middle and thus get full (classical) ZF.