# Do realizable systems always have some non-well-founded sets?

Suppose we are standing outside a realizable system which admits CZF or a similar constructive set theory. Then consider the following:

So, working backwards from outside the system, is it the case that this system always has some non-well-founded sets? The internal logic might not be able to see them, of course.

• This is purely an idle curiosity that arose while reading about domain theory. Feel free to send this to MSE or MO if it's off-topic on CS Theory. Commented Aug 3, 2023 at 14:52
• The interest in constructive or non-well-founded set theory has mostly been driven by CS in recent decades. Commented Aug 3, 2023 at 16:52

You are using the wrong definition of well-foundedness.

Let $$R \subseteq A \times A$$ be a relation. Consider the following definitions:

1. $$R$$ is inductive when for all $$B \subseteq A$$, if $$\forall x \in A . (\forall y \in A . y R x \Rightarrow y \in B) \Rightarrow x \in B$$ then $$B = A$$.

2. $$R$$ has the minimal subset property when every inhabited set $$B \subseteq A$$ has an element $$x \in B$$ such that, for all $$y \in A$$, if $$y R x$$ then $$y \not\in B$$.

3. $$R$$ has no infinite decreasing chains when there is no $$a : \mathbb{N} \to A$$ such that $$a_{n+1} R a_n$$ for all $$n \in \mathbb{N}$$.

These conditions are classically equivalent, but not intuitionistically. The one that makes sense intuitionistically is the "$$R$$ is inductive".

CZF and most material set theories either assume as an axiom, or prove from other axioms, that $$\in$$ is inductive.

As far as realizability models of constructive set theories go, you can choose whether you want them to satisfy the $$\in$$-induction axiom. (People usually do.)

CZF includes the $$\in$$-induction axiom, which is the constructively sensible version of the foundation axiom. So everything in one of its models is well-founded in that sense.

However, while I'm no expert, I think this might not be a particularly definitive property. For instance, starting with a (pre)topos, you get a model of CZF/IZF/etc. by considering well-founded trees built using the (pre)topos. But you can also take non-well-founded trees to get models of non-well-founded set theories. I'm not sure there is anything more going on in realizability models of CZF than this—the model construction explicitly picking out objects so that $$\in$$ is well-founded.