Does Regularity schema imply $\in$-induction when added to first order Zermelo set theory? That $\in$-induction fails to be a theorem schema of first order Zermelo + Foundation (see here), then it appears that it is more eligible to replace axiom of Regularity (Foundation) by a Regularity schema:
Axiom Schema of Regularity: if $\varphi(x,y_1,...,y_n)$ is a formula in which only symbols $``x,y_1,..,y_n"$ occur free (and only free), and in which the symbol $``z"$ doesn't occur, and $\varphi(z,y_1,..,y_n)$ is the formula obtained from formula $\varphi(x,y_1,..,y_n)$ by merely replacing each occurrence of the symbol $``x"$ in it by the symbol $``z"$, then
$\forall y_1,..,y_n [\exists x (\varphi(x,y_1,..,y_n)) \to \exists x (\varphi(x,y_1,..,y_n) \wedge \not \exists z \in x (\varphi(z,y_1,..,y_n)))]$
is an axiom.
In short this says: $\exists \varphi(x) \to \neg \forall \varphi(x) \exists \varphi(y) \in x$ (parameters allowed)
It is clear that this is a schematic rendering of axiom of foundation, by re-presenting it in terms of predicates instead of sets.
Now I think that first order Zermelo + Regularity schema would imply $\in$-induction.
Is that correct?
 A: Yes; the axiom schemas of regularity and $\in$-induction are equivalent, in fact by first-order logic alone.
The argument is clearest presented in the language of classes, in the style of NBG set theory. To make this an argument in $Z$, just replace each mention of a class $C$ with a formula $\varphi(x,y_1,\ldots,y_n)$, viewed as a predicate on $x$ with parameters $y_1,\ldots,y_n$.
In terms of classes, the instance of $\in$-induction for a given class $C$ says “If $C$ is $\in$-hereditary, then $C$ contains all sets.”  Similarly, the instance of regularity for a given class $D$ says: “if $D$ is inhabited, then $D$ has an $\in$-minimal element.”
But “$\in$-hereditary” is dual to “has an $\in$-minimal element”, in the sense that a class $C$ is hereditary precisely if its complement $\bar{C}$ does not have an $\in$-minimal element, and “contains all sets” is dual to “is inhabited” in the same sense.
So we have a chain of equivalent statements, using purely first-order logic:


*

*If $C$ is $\in$-hereditary, then $C$ contains all sets

*(contrapositive) If $C$ does not contain all sets, then $C$ is not $\in$-hereditary.

*(duality as noted above) If $\bar{C}$ is inhabited, then $\bar{C}$ has an $\in$-minimal element.


So this shows: the instance of $\in$-induction for any class $C$ is equivalent to the regularity for its complement $\bar{C}$, and vice versa.
Going back to the first-order axiom-scheme versions, we get that an arbitrary instance of $\in$-induction, for some formula $\varphi(x,y_1,\ldots,y_n)$, is equivalent to the instance of regularity for the complementary formula $\lnot \varphi(x,y_1,\ldots,y_n)$; and similarly, every instance of regularity for a formula $\varphi$ is equivalent to the instance of $\in$-induction for $\lnot \varphi$.
A: I'll re-present the answer of Lumsdaine that both schemes are equivalent in Classical first order logic, but in a more direct manner.
I'll start with $\in$-induction to end up in Regularity scheme, using only
Classical First order logic with membership.
$\forall x [\forall y \in x (\varphi(y)) \to \varphi(x)] \to \forall x (\varphi(x))$, we negate both sides to get:
$\neg\forall x (\varphi(x)) \to \neg \forall x [\forall y \in x (\varphi(y)) \to \varphi(x)]$
$\exists x (\neg \varphi(x)) \to \exists x [\forall y \in x (\varphi(y)) \wedge \neg \varphi(x)]$
Let $ \neg\varphi \iff \psi $, then by rule of excluded middle: $\varphi \iff \neg \psi$, then:
$\exists x (\psi(x)) \to \exists x [\forall y \in x (\neg\psi(y)) \wedge \psi(x)]$
$\exists x (\psi(x)) \to \exists x [\psi(x)\wedge\not \exists y \in x (\psi(y))  ]$
Which is the regularity schema. 
So both $\in$-induction and Regularity schema are reformulations of each other in classical first order logic with membership $\in$.
Also there is another way, albeit indirect, to show this equivalence.
Lets say that a predicate $\varphi$ is ascending if when it is fulfilled by all members of a set then it is fulfilled by that set itself (i.e. it meets the antecedent of $\in$-induction). On the other hand lets say that a predicate $\varphi$ is descending if when it is fulfilled by a set then there must be an element of that set that fulfills it. Now a property is said to be universal if it is fulfilled by all sets, and inhabited if it is fulfilled by at least one set.


*

*Regularity scheme say that all inhabited predicates are
non-descending. 

*$\in$-induction scheme says that all ascending predicates are universal.


Now if we assume 1. then clearly any counter-example to 2. would be a descending predicate thus violating the consequent of 1.! So 1. implies 2.
Now if we assume 2. then suppose that $\varphi$ is inhabited and descending, then $\neg \varphi$ is ascending, and thus $\varphi$ would violate the consequent of $\in$-induction for predicate $\neg \varphi$. So 2. implies 1.
Thus $ 1. \iff 2. $ 
However this indirect argument of equivalence also requires the law of excluded middle, and so it is only valid in classical first order logic.
