Some cute observations about computably saturated models

A model of a first-order theory $T$ is said to be computably saturated (old fashioned terminology is: recursively saturated) if it satisfies all its finitely realizable computable types (in finitely many parameters). A type $p(x,\bar y)$ is computable if the set of Gödel codes of the formulas in it is computable. A type $p(x,\bar a)$ is finitely realizable over a model $M$ with parameters $\bar a\in M$ if for every finite set $A$ of formulas from $p(\bar a,x)$, there is some $b\in M$ such that $\varphi(b,\bar a)$ holds in $M$ for every $\varphi(x,\bar y )\in A$.

I am particularly interested in computably saturated models of my two favorite theories Peano Arithmetic ${\rm PA}$ and set theory ${\rm ZFC}$. These models have many remarkable properties. For instance, countable computably saturated models have plenty of automorphisms. If $M\models{\rm PA}$ is a countable computably saturated model and $a\in M$ is not definable, then there is an automorphism which moves $a$. Indeed, given two elements $a$ and $b$ of the same type in $M$, there is an automorphism of $M$ moving $a$ to $b$. Also, if $a'$ is not definable from $a$ in $M$, then there is an automorphism fixing $a$, but moving $a'$.

As an example, let's argue that if $a$ is not definable, then there there is $b\neq a$ with the same type as $a$. For this we need to recall the notion of a standard system ${\rm SSy}(M)$ of $M$. The standard system is a collection of subsets of the (actual) natural numbers $\mathbb N$ that arise as intersections of $\mathbb N$ with definable (with parameters) sets of $M$: $${\rm SSy}(M)=\{A\subseteq\mathbb N\mid A=B\cap \mathbb N\text{ for some definable }B\subseteq M\}.$$ It is not difficult to see that a computably saturated model $M$ is ${\rm SSy}(M)$-saturated - saturated for every type (coded) in the standard system. Conversely, if $M$ is computably saturated, then ${\rm tp}(a)$, the type of $a$, is in ${\rm SSy}(M)$ for every $a\in M$. Now consider the type $p(x,a)$ consisting of formulas in ${\rm tp}(a)$ together with the assertion $x\neq a$. Clearly $p(x,y)$ is in the standard system, since ${\rm tp}(a)$ is. So it suffices to argue that it is finitely realizable, but this follows trivially from the fact that $a$ is not definable.

All the same machinery works for computably saturated models of ${\rm ZFC}$ In particular, computably saturated models of ${\rm ZFC}$ have lots of automoprhisms.

At a recent JAF meeting, we were chatting about automorphisms of computably saturated models with Roman Kossak and Michał Godziszewski, when the following cute question came up. Is it possible to have a countable computably saturated model $M$ of ${\rm ZFC}$ such that every automorphism of its natural numbers $\mathbb N^M$ extends to an automorphism of $M$? Note that $\mathbb N^M$ must be computably saturated because $M$ is, so it has many automorphisms. We thought about it some more with Corey Switzer and finally realized that this is not possible. My guess is that this is all folklore.

Theorem Suppose $M\models{\rm ZFC}$ is a countable computably saturated model, then there is an automorphism of $\mathbb N^M$ that does not extend to an automorphism of $M$.

Proof: Fix any nonstandard natural number $a\in M$. The model $M$ thinks that there is a least number $a'$ above all numbers definable over $\mathbb N^M$ by formulas of length less than $a$. In particular, it must be the case that $a'$ is not definable from $a$ because $M$ is correct about satisfaction for standard formulas over $\mathbb N^M$ and $a$ was chosen to be nonstandard. Thus, there is an automorphism of $\mathbb N^M$ which fixes $a$ but moves $a'$. But this automorphism cannot extend to $M$ because over $M$ $a'$ is definable from $a$.

The above result holds with $\mathbb N^M$ replaced by any computably saturated substructure of $M$ that is a set in $M$ because all the proof used was that $M$ has a satisfaction relation for $\mathbb N^M$.

Another random question that came up in the discussion, curtesy of Corey, was whether a non-computably saturated model of ${\rm ZFC}$ can have its natural numbers be computably saturated. The answer is easily seen to be yes.

Theorem: There is a model $M\models{\rm ZFC}$ which is not computably saturated, but its natural numbers are computably saturated.

Proof: Suppose $\bar M\models{\rm ZFC}+V={\rm HOD}$ (without getting into technicalities, $V={\rm HOD}$, the assertion that every set is hereditarily ordinal definable, says that $M$ has a definable well-ordering, and hence definable Skolem functions) is computably saturated. So $\mathbb N^{\bar M}$ is computably saturated as well. Now let $M={\rm Scl}(\mathbb N^{\bar M})$ be the Skolem closure in $\bar M$ of the set of its natural numbers. It is not difficult to see that $M$ cannot be computably saturated. Consider the type $p(x,\omega)$ (using the single parameter $\omega\in M$) asserting that $x$ is an ordinal and for every formula $\varphi(y,z)$ asserting that for every $n\in\omega$, if there is a unique $z$ such that $\varphi(n,z)$, then $x>z$. Clearly $p(x,\omega)$ is computable and finitely realizable in $M$, but it is not realized by the definition of $M$.

Roman Kossak claims, but I don't know the argument, that we can even construct such $M$ to be rigid (meaning that it would have no automorphisms), and hence very far from computably saturated.

Thanks Kameryn Williams for pointing out the following result.

Theorem: Suppose $M\models{\rm ZFC}$ is non-standard. Then $\mathbb N^M$ is computably saturated.

Proof: By a classical theorem of Lachlan, having a full satisfaction class implies computable saturation [1].

A full satisfaction class is the ${\rm PA}$ terminology for a truth predicate - a subset of the model consisting of Gödel codes of formulas (including non-standard formulas) satisfying Tarskian truth conditions. A truth predicate gives a coherent definition of what is true in the model including a truth interpretation for non-standard formulas. Kotlarski, Krajewski, and Lachlan showed a partial converse that a countable computably saturated model always has a full satisfaction class [2].

An excellent source on everything you need to know about computably saturated models of ${\rm PA}$ is Roman's and Jim Schmerl's book [3]. Most results there generalize to computably saturated models of ${\rm ZFC}$, but there is not one good definitive source for results on these models, although people including myself, Joel Hamkins and Michał have written papers about them. See for example, [4] and [5] for interesting constructions with computably saturated models of ${\rm ZFC}$.


  1. A. H. Lachlan, “Full satisfaction classes and recursive saturation,” Canad. Math. Bull., vol. 24, no. 3, pp. 295–297, 1981. Available at:
  2. H. Kotlarski, S. Krajewski, and A. H. and Lachlan, “Construction of satisfaction classes for non-standard models,” Canad. Math. Bull., vol. 24, no. 3, pp. 283–293, 1981.
  3. R. Kossak and J. H. Schmerl, The structure of models of Peano arithmetic, vol. 50. The Clarendon Press, Oxford University Press, Oxford, 2006, p. xiv+311. Available at:
  4. J. D. Hamkins and R. Yang, “Satisfaction is not absolute,” to appear in the Review of Symbolic Logic, pp. 1–34, 2014. Available at:
  5. 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. Available at: