Computably saturated models of ZFC

Let $\mathcal L$ be any computable first-order language. A type $p(\bar x,\bar y)$ in $\mathcal L$ is said to be computable if the collection of Gödel codes of the formulas in the type $$\{\ulcorner \varphi\urcorner\mid \varphi\in p(\bar x,\bar y)\}$$ is a computable set. A model $M$ of $\mathcal L$ is said to be computably saturated if for every tuple $\bar a\in M$ and every computable type $p(\bar x,\bar y)$, whenever $p(\bar x,\bar a)$ is finitely realizable in $M$, then $p(\bar x,\bar a)$ is realized: there is a tuple $\bar b\in M$ such that for every $\varphi\in p(\bar x,\bar y)$, $M\models\varphi(\bar b,\bar a)$. It is not difficult to see that any model $M$ of cardinality $\kappa$ has a computably saturated elementary extension of cardinality $\kappa$. We build the elementary extension in $\omega$-many steps, at each step realizing all finitely realizable computable types with parameters from the previous stage. Observe that any computably saturated model of ${\rm ZFC}$ must have nonstandard natural numbers because it realizes the computable type $$p(x)=\{x>\underbrace{1+\cdots+1}_{n\text{-times}}\mid n\in\mathbb N\}.$$ Computable saturation was introduced in [1].

Let's call a model of ${\rm ZFC}$ $\omega$-nonstandard if it has nonstandard natural numbers. In the model theory of $\omega$-nonstandard models of ${\rm ZFC}$ (as in the model theory of nonstandard models of ${\rm PA}$) one of the most important notions is the standard system introduced by Friedman in [2]. The standard system of an $\omega$-nonstandard model of ${\rm ZFC}$ is a collection of subsets of $\mathbb N$ consisting of the traces of sets in $M$ on the natural numbers: $${\rm SSy}(M)=\{A\cap \mathbb N\mid A\in M\}.$$ Standard systems are clearly Boolean algebras. Standard systems are closed under computability: whenever $A$ is in it and $B$ is computable from $A$, then $B$ is in it. To see this, fix $A\in {\rm SSy}(M)$ and let $B$ be computed from $A$ by a program $p$. The set $A=A^*\cap \mathbb N$ for some $A^*\in M$ and we can assume without loss that $A^*\subseteq\mathbb N^M$. The computation of program $P$ with oracle $A^*$ inside $M$ agrees with the actual computation of $p$ with oracle $A$ on the standard part, which is $B$. In particular, it follows that a standard system has all computable sets, and so computable theories such as ${\rm PA}$ and ${\rm ZFC}$ are (coded) in the standard system. Finally, whenever a set $T$ in a standard system codes an infinite binary tree, the standard system must have some infinite branch through $T$. Such a set $T$ must have come from a set $T^*\in M$, which has to look like a binary tree up to some nonstandard level (because otherwise the true natural numbers would be definable in $M$). So we fix some node $c$ on a nonstandard level of $T^*$ and its predecessors in $T^*$ give a branch through $T$. Observe also if $M$ and $N$ are $\omega$-nonstandard models of ${\rm ZFC}$ such that $\mathbb N^M$ is an initial segment of $\mathbb N^N$, then ${\rm SSy}(M)\subseteq {\rm SSy}(N)$. The reason is that if a set $A\in {\rm SSy}(M)$, then there is a nonstandard natural number $a\in M$ such that the characteristic function of $A$ is coded on the standard part of the binary expansion of $a$, and indeed $M$ has such numbers arbitrarily low above the standard $\mathbb N$.

An $\omega$-nonstandard model $M\models{\rm ZFC}$ is said to be ${\rm SSy}(M)$-saturated if for every type $p(\bar x,\bar y)$ (coded) in ${\rm SSy}(M)$, whenever there is $\bar a\in M$ such that $p(\bar x,\bar a)$ is finitely realizable, then $p(\bar x,\bar a)$ is realized. Since ${\rm SSy}(M)$ has all the computable sets, ${\rm SSy}(M)$-saturated models are computably saturated. But the converse holds as well. To see this, fix a type $p(\bar x,\bar y)$ in ${\rm SSy}(M)$ and let $A\in M$ such that $A\cap\mathbb N=\{\ulcorner\varphi\urcorner\mid \varphi\in p(\bar x,\bar y)\}$. Suppose that for $\bar a\in M$, $p(\bar x,\bar a)$ is finitely realizable. Consider the computable type $$p^*(\bar x,\bar y,z)=\{\varphi(\bar x,\bar y)\leftrightarrow \ulcorner\varphi\urcorner\in z\mid \varphi\text{ is a formula}\}.$$ Since $p(\bar x,\bar a)$ is finitely realizable, then so is $p^*(\bar x,\bar a,A)$, but the realization of $p^*(\bar x,\bar a,A)$ also realizes $p(\bar x,\bar a)$. Standard system saturation was introduced by Wilmers in an unpublished 1975 thesis.

We can use standard system saturation to show several key properties of computably saturated models. The standard system of a computably saturated model has all the types of its elements ($\text{tp}^M(\bar a)$ for $\bar a\in M$), and in particular its theory. Suppose $M$ is ${\rm SSy}(M)$-saturated and $\bar a\in M$. We need to show that there is $A\in M$ such that $A\cap \mathbb N=\{\ulcorner\varphi\urcorner\mid M\models\varphi(\bar a)\}$. Consider the computable type $$p(x,\bar y)=\{\varphi(\bar y)\leftrightarrow \ulcorner\varphi\urcorner\in\bar x\mid\varphi\text{ is a formula}\}.$$ Since $M$ has $\Sigma_n$-truth predicates for every true natural number $n$, $p(x,\bar a)$ is finitely realizable in $M$, and thus there is $A\in M$ realizing $p(\bar x,\bar a)$. Once we have that all types are in the standard system, we obtain a remarkable characterization of countable computably saturated models.

Theorem: Countable computably saturated models $M$ and $N$ of ${\rm ZFC}$ are isomorphic if and only if they have the same theory and the same standard system. Indeed, if $\text{tp}^M(\bar a)=\text{tp}^N(\bar b)$, then there is an isomorphism taking $\bar a$ to $\bar b$.

Proof: This is a back-and-forth argument. Let's extend the partial isomorphism taking $\bar a$ to $\bar b$ one more step. Fix $c\in M$. Then $\text{tp}(c,\bar a)\in {\rm SSy}(M)={\rm SSy}(N)$ and $p(x,\bar y)=\{\varphi(x,\bar y)\mid \varphi\in \text{tp}(x,\bar y)\}$ is finitely realizable in $N$. Thus, by standard system saturation, there is $d\in N$ such that $\text{tp}(c,\bar a)=\text{tp}(d,\bar b)$.

Corollary: Countable computably saturated models $M\models{\rm ZFC}$ have many automorphisms. Whenever $a,b\in M$ are such that $\text{tp}(a)=\text{tp}(b)$, then there is an automorphism of $M$ taking $a$ to $b$.

Computably saturated models of ${\rm ZFC}$ arise naturally as follows. If $M\models{\rm ZFC}$ is an element of an $\omega$-nonstandard model of ${\rm ZFC}$, then $M$ is computably saturated. To see this, fix a computable type $p(\bar x,\bar y)$ and a tuple $\bar a\in M$ such that $p(\bar x,\bar a)$ is finitely realizable. Also fix a set $A\in N$ such that $A\cap \mathbb N$ codes $p(\bar x,\bar y)$. Since $M$ is a set in $N$, $N$ has a truth predicate for $M$, which by absoluteness of satisfaction must be correct for standard formulas. The model $N$ sees, for every true natural number $n$, that $M$ realizes all $\varphi(\bar x,\bar a)$ such that $\ulcorner\varphi\urcorner\in A\cap n$. But then there must be some nonstandard $c\in N$ such that $N$ thinks that $M$ realizes all $\varphi(\bar x,\bar a)$ such that $\ulcorner\varphi\urcorner\in A\cap c$. Any such realization $\bar b$ realizes $p(\bar x,\bar a)$ because $A\cap c$ includes all standard assertions.

Here are some other remarkable results about computably saturated models of ${\rm ZFC}$.

Theorem:: Every computably saturated model $M\models{\rm ZFC}$ has an elementary rank initial segment $V_\alpha^M\prec M$ [3].

Proof: Consider the computable type $p(x)$ consisting of assertions $$\forall \ulcorner\varphi\urcorner\in\Sigma_n\,\text{Tr}_{\Sigma_n}(\ulcorner\varphi\urcorner)\leftrightarrow \text{Tr}_{\Delta_0}(\ulcorner x\models\varphi\urcorner)$$ for every $n$ (where $\text{Tr}_{\Sigma_n}$ is a $\Sigma_n$-truth predicate) together with the assertion "$x$ is a rank initial segment".

The following observation was the key to our theorem with Joel Hamkins that the collection of all countable computably saturated models satisfies the Hamkins Multiverse Axioms [4].

Theorem: Every countable computably saturated model of ${\rm ZFC}$ has an isomorphic copy of itself as an element which it thinks is countable and $\omega$-nonstandard.

Proof: Suppose $N$ is countable and computably saturated. The theory $\mathcal T$ of $N$ is in ${\rm SSy}(N)$ and so we can fix a theory $\mathcal T^*\in N$ such that $\mathcal T^*\cap\mathbb N=\mathcal T$. The model $N$ sees that $\mathcal T^*\cap n$ is consistent for every true natural number $n$ and therefore $N$ has some nonstandard natural number $c$ such that it thinks that $\mathcal T^*\cap c$ is consistent. Thus, $N$ has a model of $\mathcal T^*\cap c$. But then $N$ also thinks that $\mathcal T^*\cap c$ also has an $\omega$-nonstandard model $M$. Since $\mathbb N^N$ is an initial segment of $\mathbb N^M$, the two models have the same standard system and by construction they have the same theory. Therefore $M\cong N$.

For the final result I want to mention, let's recall that a truth predicate for an $\omega$-nonstandard model $M\models{\rm ZFC}$ is a subset $T\subseteq M$ such that in the structure $\langle M,\in,T\rangle$, $T$ satisfies the Tarskian truth conditions for $\langle M,\in\rangle$. In particular, $T$ must be a truth predicate for standard formulas. A set $T\subseteq M$ is a partial truth predicate if in $\langle M,\in,T\rangle$, there is a nonstandard number $c$ such that $T$ restricted to formulas of length less than $c$ satisfies Tarskian truth conditions.

Theorem: The following are equivalent for a countable $\omega$-nonstandard $M\models{\rm ZFC}$.

  1. $M$ is computably saturated.
  2. $M$ has a partial truth predicate $T$ such that $\langle M,\in,T\rangle$ satisfies ${\rm ZFC}$ in the extended language.
  3. $M$ has a truth predicate.

The same result for models of ${\rm PA}$ was shown by Kotlarski, Krajewski, and Lachlan [5], [6]. In his dissertation Bartosz Wcisło showed that a truth predicate can be used to define a partial truth predicate preserving ${\rm PA}$ and Michał Godzisgewski observed that with this new result the theorem extends to models of ${\rm ZFC}$. Note that it is impossible to extend condition $(3)$ to say that $\langle M,\in,T\rangle\models{\rm ZFC}$ because any such $M$ would be a model of $\text{Con}({\rm ZFC})$.

References

  1. J. Barwise and J. Schlipf, “An introduction to recursively saturated and resplendent models,” J. Symbolic Logic, vol. 41, no. 2, pp. 531–536, 1976.
  2. H. Friedman, “Countable models of set theories,” in Cambridge Summer School in Mathematical Logic (Cambridge, 1971), Berlin: Springer, 1973, pp. 539–573. Lecture Notes in Math., Vol. 337.
  3. J. P. Ressayre, “Introduction aux modèles récursivement saturés,” in Séminaire Général de Logique 1983–1984 (Paris, 1983–1984), vol. 27, Univ. Paris VII, Paris, 1986, pp. 53–72.
  4. V. Gitman and J. D. Hamkins, “A natural model of the multiverse axioms,” Notre Dame J. Form. Log., vol. 51, no. 4, pp. 475–484, 2010.
  5. H. Kotlarski, S. Krajewski, and A. H. Lachlan, “Construction of satisfaction classes for nonstandard models,” Canad. Math. Bull., vol. 24, no. 3, pp. 283–293, 1981.
  6. A. H. Lachlan, “Full satisfaction classes and recursive saturation,” Canad. Math. Bull., vol. 24, no. 3, pp. 295–297, 1981.