In posting "[Does Regularity schema imply $\in$-induction when added to first order Zermelo set theor?](https://mathoverflow.net/questions/314780/does-regularity-schema-imply-in-induction-when-added-to-first-order-zermelo-s)"


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?
> 
> 
> 



Are Regularity schema and $\in$-induction schema equivalent in intuitionistic logic?
As discussed in the [nLab link](https://ncatlab.org/nlab/show/well-founded+relation) 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.


