Recall that a model $M$ of a first-order theory $T$ (in a computable language $\mathcal{L}$) is *computably saturated* if for every finite tuple $\bar{a} \in M$ and every computable partial type $\Sigma(\bar{x},y)$, if $\Sigma(\bar{a},y)$ is consistent, then there is a $b \in M$ such that $M \models \Sigma(\bar{a},b)$.


Schmerl proved (a more general version of) a fairly surprising fact: Any countable, computably saturated model of $\mathsf{PA}$ is the Skolem hull of an indiscernible sequence. This is intuitively surprising because on the one hand models with properties resembling saturation are typically regarded as 'large,' whereas Ehrenfeucht-Mostowski models (Skolem hulls of indiscernible sequences) are typically regarded as 'small.' One of the lessons of modern neo-stability-based model theory is that while indiscernible sequences are nice, Morley sequences are nicer, so it seems natural to me to wonder if this result can be generalized, at least somewhat, to Morley sequences.

To avoid spending a lot of time developing the general concept of Morley sequences and to increase the chances that this question will be answered, I will restrict attention to two special cases, one of which is already familiar in the model theory of $\mathsf{PA}$.

Recall that a type $p \in S_1(M)$ (with $M$ a model) is *definable* (without parameters) if for any $\mathcal{L}$-formula $\varphi(x,\bar{y})$, there is a formula $\psi_\varphi(\bar{y})$ such that for every $\bar{b} \in M^{\bar{y}}$, $\varphi(x,\bar{b}) \in p(x)$ if and only if $M \models \psi_\varphi(\bar{b})$. Given a definable type $p \in S_1(M)$, the formulas $\psi_{\varphi}(\bar{y})$ defines a unique type $p|A$ over any set of parameters $A$ given by
$$\{ \varphi(x,\bar{b}) : \varphi \in \mathcal{L}\text{, }\bar{b} \in A\text{, }\psi_\varphi(\bar{b})\}.$$

Fix a definable type $p \in S_1(M)$. Let $a_0$ be a realization of $p$. For each $n > 0$, let $a_n$ be a realization of $p|a_0\dots a_{n-1}$. This sequence is always indiscernible. An arbitrary indiscernible sequence $I$ is a *Morley sequence in $p$* if for every increasing $n$-tuple $\bar{b} \in I$, $\bar{b} \equiv a_0\dots a_{n-1}$.

> **Question 1.** Is there a completion $T$ of $\mathsf{PA}$ and a definable type $p$ over $T$ such that the Skolem hull of some Morley sequence in $p$ is computably saturated?

Fix a set of parameters $A$ and an ultrafilter $\mathcal{U}$ on $A$. For any set of parameters $B \supseteq A$, there is a unique complete type $p_{\mathcal{U}}|A$ defined by
$$\{ \varphi(x,\bar{b}) : \varphi \in \mathcal{L}\text{, }\bar{b} \in B\text{, }\{a \in A : \varphi(a,\bar{b})\} \in \mathcal{U}\}.$$

Let $a_0$ be a realization of $p_{\mathcal{U}} |A$. For each $n > 0$, let $a_n$ be a realization of $p_{\mathcal{U}}|Aa_0\dots a_{n-1}$. This is always an $A$-indiscernible sequence. A *Morley sequence in $p_{\mathcal{U}}$* is an indiscernible sequence $I$ such that for any increasing $n$-tuple $\bar{b} \in I$, $\bar{b} \equiv a_0\dots a_{n-1}$.

> **Question 2.** Is there a completion $T$ of $\mathsf{PA}$ and an ultrafilter $\mathcal{U}$ on the prime model of $T$ such that the Skolem hull of some Morley sequence in $p_{\mathcal{U}}$ is computably saturated?

Note that in both cases, while we say 'some' Morley sequence, one can show that if there is such a Morley sequence, then a Morley sequence of order type $\mathbb{Q}$ will suffice.

---

EDIT: Here I'll give a purely syntactic formulation of Question 1.

For any definable type $p(x)$ and formula $\varphi(x,\bar{y})$, I'll write $d_px \varphi(x,\bar{y})$ for the formula $\psi(\bar{y})$ with the property that $\varphi(x,\bar{b}) \in p(x)$ if and only if $\psi(\bar{b})$ holds. Note that $d_p x$ behaves syntactically like a quantifier, bounding the variable $x$.

For any definable type $p(x)$ and $n < \omega$, $p^{\otimes n}(x_0\dots x_{n-1})$ is the $n$-type defined by
$$ \{\varphi(x_0,\dots,x_{n-1}) : T \vdash d_p x_0 \dots d_p x_{n-1} \varphi(x_0,\dots,x_{n-1})\}.$$
(This is the same thing as $\mathrm{tp}(a_0\dots a_{n-1})$ in the setup of Question 1.) 

Explicitly add Skolem functions to the language of $\mathsf{PA}$.

> **Question 1 (syntactic formulation).** Does there exist a completion $T$ of $\mathsf{PA}$ and a definable type $p(x)$ over $T$ such that for any computable partial type $\Sigma(\bar{x},y)$, if $\Sigma(\bar{x},y) \cup p^{\otimes n}(\bar{x})$ is consistent, then there is an $m$ and a Skolem term $t(\bar{z}_0x_0\bar{z}_1x_1\dots\bar{z}_{n-1}x_{n-1}\bar{z}_n)$ with each $\bar{z}_i$ an $m$-tuple such that
$$ p^{\otimes (n+m(n+1))}(\bar{z}_0x_0\dots x_{n-1}\bar{z}_n) \vdash \Sigma(\bar{x},t(\bar{z}_0x_0\dots x_{n-1}\bar{z}_n))?$$