1
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Corbin
    Aug 3, 2023 at 14:52
  • 1
    $\begingroup$ The interest in constructive or non-well-founded set theory has mostly been driven by CS in recent decades. $\endgroup$ Aug 3, 2023 at 16:52

2 Answers 2

3
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.