<p>You are using the wrong definition of well-foundedness.</p>
<p>Let <span class="math-container">$R \subseteq A \times A$</span> be a relation. Consider the following definitions:</p>
<ol>
<li><p><span class="math-container">$R$</span> is <strong>inductive</strong> when for all <span class="math-container">$B \subseteq A$</span>, if <span class="math-container">$\forall x \in A . (\forall y \in A . y R x \Rightarrow y \in B) \Rightarrow x \in B$</span> then <span class="math-container">$B = A$</span>.</p>
</li>
<li><p><span class="math-container">$R$</span> has the <strong>minimal subset property</strong> when every inhabited set <span class="math-container">$B \subseteq A$</span> has an element <span class="math-container">$x \in B$</span> such that, for all <span class="math-container">$y \in A$</span>, if <span class="math-container">$y R x$</span> then <span class="math-container">$y \not\in B$</span>.</p>
</li>
<li><p><span class="math-container">$R$</span> has <strong>no infinite decreasing chains</strong> when there is no <span class="math-container">$a : \mathbb{N} \to A$</span> such that <span class="math-container">$a_{n+1} R a_n$</span> for all <span class="math-container">$n \in \mathbb{N}$</span>.</p>
</li>
</ol>
<p>These conditions are classically equivalent, but not intuitionistically. The one that makes sense intuitionistically is the &quot;<span class="math-container">$R$</span> is inductive&quot;.</p>
<p>CZF and most material set theories either assume as an axiom, or prove from other axioms, that <span class="math-container">$\in$</span> is inductive.</p>
<p>As far as realizability models of constructive set theories go, you can choose whether you want them to satisfy the <span class="math-container">$\in$</span>-induction axiom. (People usually do.)</p>

CC BY-SA 4.0
2023-08-03T22:18:44.390Z
2023-08-03T22:46:07.743Z
2023-08-03T22:46:07.743Z
Andrej Bauer
<p>CZF includes the <span class="math-container">$\in$</span>-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.</p>
<p>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 <span class="math-container">$\in$</span> is well-founded.</p>

CC BY-SA 4.0
2023-08-03T17:10:32.157Z
2023-08-03T17:10:32.157Z
Dan Doel
<p>Suppose we are standing outside a <a href="https://en.wikipedia.org/wiki/Realizability" rel="nofollow noreferrer">realizable</a> system which admits CZF or a similar <a href="https://en.wikipedia.org/wiki/Constructive_set_theory" rel="nofollow noreferrer">constructive set theory</a>. Then consider the following:</p>
<ul>
<li><a href="https://ncatlab.org/nlab/show/excluded+middle" rel="nofollow noreferrer">LEM</a> is not realized (e.g. <a href="https://math.stackexchange.com/a/4314463/425071">this MSE answer</a>)</li>
<li>The traditional foundation axiom (all sets have a least element when ordered by elementhood) implies LEM (e.g. <a href="https://us.metamath.org/ileuni/regexmid.html" rel="nofollow noreferrer"><code>regexmid</code> in Metamath ILE</a>)</li>
</ul>
<p>So, working backwards from outside the system, is it the case that <strong>this system always has some non-well-founded sets?</strong> The internal logic might not be able to see them, of course.</p>

CC BY-SA 4.0
2023-08-03T14:52:11.767Z
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.
Corbin
CC BY-SA 4.0
2023-08-03T16:52:47.020Z
The interest in constructive or non-well-founded set theory has mostly been driven by CS in recent decades.
Martin Berger
<lo.logic><computability><set-theory><domain-theory>
Do realizable systems always have some non-well-founded sets?
Corbin
# Do realizable systems always have some non-well-founded sets?

(Asked by: username_0 on 2023-08-03)

Suppose we are standing outside a [realizable](https://en.wikipedia.org/wiki/Realizability) system which admits CZF or a similar [constructive set theory](https://en.wikipedia.org/wiki/Constructive_set_theory). Then consider the following:

* [LEM](https://ncatlab.org/nlab/show/excluded+middle) is not realized (e.g. [this MSE answer](https://math.stackexchange.com/a/4314463/425071))
* The traditional foundation axiom (all sets have a least element when ordered by elementhood) implies LEM (e.g. [`regexmid` in Metamath ILE](https://us.metamath.org/ileuni/regexmid.html))

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.

**Tags:** lo.logic, computability, set-theory, domain-theory

> **Comments:**
> **username_0**: 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.  
> **username_1**: The interest in constructive or non-well-founded set theory has mostly been driven by CS in recent decades.  

---

## 2 answers

### Answer by username_2 on 2023-08-03. Score: 3 | Accepted answer

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.)


---

### Answer by username_3 on 2023-08-03. Score: 2

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.


---

