- A relation $(X,\prec)$ is well-founded if for any subset $S\subseteq X$ which is inductive, in the sense that $y\in S$ for all $y\prec x$ implies $x\in S$, in fact $S=X$.
This is classically equivalent to the more usual definition, but constructively more reasonable. Now in constructive set theories such as CZF, one often finds a different axiom of "foundation" called set-induction or epsilon-induction:
- For any formula $\phi$, if $\phi(x)$ for all $x\in y$ implies $\phi(y)$ for any set $y$, then in fact $\phi(x)$ is true for all sets $x$.
This certainly implies that $\in$ is well-founded on any transitive set in the sense above, and the converse is true if every set has a transitive closure and you have the full axiom of separation, since from any transitive set $x$ you can form $\lbrace y\in x \mid \phi(y) \rbrace$ and conclude that it is all of $x$.
Now classically, one can show that the axiom of foundation is consistent, relative to the other axioms of set theory, by simply restricting any model to the submodel of well-founded sets. I think you can do this in CZF for the version of "foundation" I stated above, that every transitive set is well-founded. My question is, can you do anything similar with set-induction? I care most about CZF, but I'd also be interested to know about results in any other theory lacking the full axiom of separation.
(BTW, it's possible one might have to fiddle a little bit with what I mean by "the other axioms of CZF" to make this nontrivial. For one thing, let's drop the axiom of infinity, since I see no guarantee that $\omega$ would be "strongly well-founded" in the necessary sense.)