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}$.
References
- A. H. Lachlan, “Full satisfaction classes and recursive saturation,” Canad. Math. Bull., vol. 24, no. 3, pp. 295–297, 1981.
- 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.
- 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.
- J. D. Hamkins and R. Yang, “Satisfaction is not absolute,” to appear in the Review of Symbolic Logic, pp. 1–34, 2014. Available at: http://wp.me/p5M0LV-Gf
- 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.