= Solution
Let $M\subseteq N$ be transitive models of <ZFC> containing the set relation $R$ and its underlying set $X$. If $M$ judges $R$ well founded, it has an <ordinal rank function for a relation> $\rho\in M$ by the preceding rank characterization. Being a function to <ordinals> and satisfying
$$
\forall x,y\in X\ (xRy\Rightarrow\rho(x)<\rho(y))
$$
is absolute: the values are actual ordinals and the checks use only <bounded formulas in set theory>. The same rank function exists in $N$, so $N$ judges $R$ well founded.
Conversely, if $M$ judged it not well founded, it would contain a nonempty set $Y$ with no $R$-minimal element. The property of this particular $Y$ is bounded and remains true in $N$, contradicting well-foundedness there. Thus
$$
\boxed{M\models\text{“}R\text{ is well founded”}
\iff N\models\text{“}R\text{ is well founded”}.}
$$
This is <absoluteness of well-foundedness>. The hypotheses that both models are transitive and satisfy <ZFC> matter; a small transitive set without sufficient recursion axioms need not contain the required rank witness.
Back to article page
