Characterizing relative decidability
in terms of model completeness

Abstract

A theory $T$ is said to be relatively decidable if for every model of $T$, one can compute the elementary diagram of that model from its atomic diagram together with $T$. We verify a conjecture of Chubb, Miller, and Solomon by showing that for complete theories $T$, $T$ is relatively decidable if and only if $T$ has a conservative model complete extension of the form $T\cup \{\phi (\overline{c})\}$ where $T\vDash \exists \overline{x}\phi (\overline{x})$. We also show that no such characterization works for incomplete theories.

1 Introduction

In applied model theory, especially in the style of Robinson, one of the main tasks when studying a particular class of structures is to understand the definable sets. The strongest way to do this is to prove a quantifier elimination result, which says that every definable set can be defined by a formula without quantifiers. Chevalley’s theorem on constructible sets is exactly quantifier elimination for algebraically closed fields, while work of Seidenberg, Robinson, and Blum established quantifier elimination for differentially closed fields in characteristic zero (see [MAR00]). Many natural structures do not have quantifier elimination in their natural languages, but instead satisfy a weaker variant of quantifier elimination known as model completeness: Every definable set can be defined by both an existential formula and a universal formula. A classical example due to Tarski [TAR48] is the field of real numbers, which admits quantifier elimination in the language of ordered fields but is only model complete in the algebraic language without the ordering. Other examples of model completeness without quantifier elimination include the field ${\mathbb{Q}}_p$ of $p$-adic numbers [MAC76], the exponential field $(ℝ,\exp )$ of real numbers [WIL96], and algebraically closed fields with a generic automorphism [CH99].

One consequence of model completeness is that it yields an algorithm reducing the problem of computing membership in definable sets to membership in quantifier-free definable sets. Such an algorithm might be thought of as the weakest possible variant of quantifier elimination. Our main result is that for complete theories the existence of such an algorithm implies model completeness after naming finitely many constants. This perhaps explains the ubiquity of model completeness.

More formally, let $ℒ$ be a computable first-order language and $T$ a recursively axiomatizable first-order theory. If $T$ is model complete, then every formula $\phi (\overline{x})$ is equivalent modulo $T$ to both an existential and a universal formula. For every $𝒜\vDash T$ (with domain $\mathbb{N}$, so that it makes sense to perform computations on $𝒜$) we can use the atomic diagram of $𝒜$ to compute the elementary diagram of $𝒜$. Indeed, given a formula $\phi (\overline{x})$ and $\overline{a}\in 𝒜$, we can find quantifier-free formulas ${\psi }_{𝖳}(\overline{x},\overline{y})$ and ${\psi }_{𝖥}(\overline{x},\overline{z})$ such that

$$T\vDash \phi (\overline{x})⟷\exists \overline{y}{\psi }_{𝖳}(\overline{x},\overline{y})\text{ and }T\vDash \neg \phi (\overline{x})⟷\exists \overline{z}{\psi }_{𝖥}(\overline{x},\overline{z}).$$

Since the theory is c.e., we can search for these formulas computably. Then, using the atomic diagram of $𝒜$, we can simultaneously search for either $\overline{b}\in 𝒜$ such that $𝒜\vDash {\psi }_{𝖳}(\overline{a},\overline{b})$ (in which case we have determined that $𝒜\vDash \phi (\overline{a})$) or for $\overline{c}\in 𝒜$ such that $𝒜\vDash {\psi }_{𝖥}(\overline{a},\overline{c})$ (in which case we have determined that $𝒜\vDash \neg \phi (\overline{a})$).

Chubb, Miller, and Solomon [CMS21] named this property of $T$ relative decidability. While they defined this only for recursively axiomatizable theories, we remove this assumption by modifying the definition to allow access to the theory $T$ in the computations.

Definition 1.1.

A theory $T$ is relatively decidable if for every countable $𝒜\vDash T$ with domain $\mathbb{N}$ the theory $T$ together with the atomic diagram of $𝒜$ compute the elementary diagram of $𝒜$.

If $T$ is model complete, then not only is $T$ relatively decidable, but it is uniformly relatively decidable: There is a single algorithm (or Turing functional) that can always be used to compute the elementary diagram of a model from the atomic diagram. Chubb, Miller, and Solomon [CMS21] showed that these are the only uniformly relatively decidable theories, i.e., that $T$ is uniformly relatively decidable if and only if it is model complete. This result holds for both complete and incomplete theories.

Chubb, Miller, and Solomon provided several examples of natural theories that are relatively decidable but not uniformly relatively decidable, including the theory of $(\mathbb{N},S)$ where $S$ is the successor relation. The non-uniformity comes from the fact that in each model of $\mathrm{Th}(\mathbb{N},S)$ we must identify the unique element that has no predecessor. In particular,

$$\mathrm{Th}(\mathbb{N},S)\vDash \exists x\forall yS(y)\ne x$$

and in the language $\{S,0\}$ with an additional constant, $\mathrm{Th}(\mathbb{N},S)\cup \{\forall yS(y)\ne 0\}$ is model complete. Chubb, Miller, and Solomon [CMS21] conjectured that one can characterize relative decidability in this form.

Our main result is a confirmation of this conjecture when the theory $T$ is complete.

Theorem 1.2.

Let $T$ be a complete theory. Then $T$ is relatively decidable if and only if there is a formula $\phi (\overline{x})$ such that

1. $T\vDash \exists \overline{x}\phi (\overline{x})$, and

2. the $ℒ\cup \{\overline{c}\}$-theory $T\cup \{\phi (\overline{c})\}$ is model complete.

The difficult direction of the proof is to show that if $T$ is relatively decidable then such a formula $\phi (\overline{x})$ exists; the other implication is easy to see and is true even if the theory is not complete. The general outline is as follows. After applying standard computability-theoretic forcing techniques, for each model $𝒜$ and formula $\phi (\overline{x})$ we obtain an infinitary ${\mathrm{\Sigma }}_1$ formula $\psi (\overline{x})$, a countable disjunction of existential formulas, which is equivalent to $\phi (\overline{x})$ in $𝒜$. The difficulty is that in different models $𝒜$, we may get different ${\mathrm{\Sigma }}_1$ formulas. The heart of the proof is an elementary but intricate purely model-theoretic argument to resolve this by passing between large (saturated) and small (type-omitting) models of $T$. The argument, appearing in Section 2, is only four pages and is very much worth reading.

Our result and the result of Chubb, Miller, and Solomon in the uniform case fit into a central theme in computable structure theory that robust computational properties should arise from definability. See, e.g., the standard texts [AK00, MON21, MON26] on computable structure theory where this theme plays a central role. Usually this is at the level of a single isomorphism type, e.g., Knight [KNI86] showed that if we can enumerate a set $X$ from the atomic diagram of every copy of $𝒜$ then $X$ is enumeration reducible to the existential type of a tuple $\overline{a}$ in $𝒜$. The definability is also usually in the infinitary logic ${ℒ}_{{\omega }_1\omega }$. Because we are working with a first-order theory, compactness and omitting types allow us to reduce this definability to a model-theoretic property of finitary logic. The relationship between relative decidability and uniform relative decidability also follows the usual pattern when working with a single isomorphism type, which is that in the uniform case one does not have to name a tuple from the structure, but in the non-uniform case one does. Our result agrees with this pattern on a surface level but, while usually the uniform and non-uniform cases are essentially the same, here the non-uniform case is significantly more challenging and requires new tools, e.g., saturation and omitting types, while the uniform case required only compactness.

In the proof of the above theorem it is vital that $T$ be a complete theory. In the proof, this assumption is used in the following form: Given a sentence $\phi$, if we can show that some particular $𝒜\vDash T$ satisfies $\phi$, then every model of $T$ satisfies $\phi$. Of course, it is natural to ask whether relative decidability can be characterized for incomplete theories as well. We show that there is no such characterization. Consider the naive definition of relative decidability; it requires a universal quantifier over all models of $T$. In terms of descriptive set theory, this makes the set of relatively decidable theories a ${𝚷}_1^1$ set. On the other hand, a characterization such as that in Theorem 1.2 uses only quantifiers over finitary formulas and proofs, and so one consequence of that characterization is that the set of complete relatively decidable theories is Borel.

We show that the set of (not necessarily complete) relatively decidable theories is ${𝚷}_1^1$-complete, and in particular it is not Borel.

Theorem 1.3.

There is a language $ℒ$ such that the set

$$\{T\text{ a }ℒ\text{-theory}:T\text{ is relatively decidable}\}$$

is ${𝚷}_1^1$-Wadge-complete.

In particular, we show that given a tree , we can construct (in a relatively computable way) a theory $T_{𝔗}$ such that

$$𝔗\text{ is well-founded}⟺T_{𝔗}\text{ is relatively decidable}.$$

This implies that there is no characterization of relative decidability for incomplete theories which is simpler in form than the naive definition. In particular, we cannot prove Theorem 1.2, or any similar theorem, for arbitrary theories. The argument uses the tool of Marker extensions of theories, and we must develop the necessary definitions and lemmas, and particularly Lemma 3.2, in Section 3. The proof of Theorem 1.3 follows in Section 4. The definition of the theory and the argument that if $𝔗$ is well-founded then $T_{𝔗}$ is relatively decidable are both reasonably short. The argument that if $𝔗$ is ill-founded then $T_{𝔗}$ is not relatively decidable is quite technical.

This situation should remind the reader of omitting types. For complete theories, we have a simple characterization of when a type can be omitted: it must be non-isolated. For incomplete theories, this is sufficient but not necessary, and the sufficient and necessary conditions obtained by Casanovas and Farré [CF96] involve the well-foundedness of trees. Indeed, it is not hard to show after reading that paper that the set of omittable types is ${𝚺}_1^1$-complete.

Finally, we would like to highlight the following open problem of Goncharov:

Question 1.4 (Goncharov).

Characterize the decidable theories $T$ such that every computable model of $T$ is decidable.

The corresponding index set is ${\mathrm{\Sigma }}_{\omega +2}$; we conjecture that it is ${\mathrm{\Sigma }}_{\omega +2}$ $m$-complete. However, the methods from this paper are not applicable to this problem, as (by index set complexity calculations) to prove that the index set is ${\mathrm{\Sigma }}_{\omega +2}$ $m$-complete one would have to build decidable models $𝒜$ of $T$ such that for no $\overline{a}\in 𝒜$ is $\mathrm{Th}(𝒜,\overline{a})$ model complete.

2 Complete theories

We will require a variant of the standard omitting types theorem where, for a complete theory, we try to omit countably many partial types even if some of them may be isolated. Of course an isolated type cannot be omitted, but we can force all of its realizations to be of a certain kind. Recall that a partial type $p(\overline{x})$ is isolated if there is a formula $\phi (\overline{x})$ such that $T\vDash \exists \overline{x}\phi (\overline{x})$ and $T\vDash \forall \overline{x}(\phi (\overline{x})⟶p(\overline{x}))$. In this case we say that $\phi (\overline{x})$ isolates $p(\overline{x})$. The formula $\phi (\overline{x})$ does not necessarily have to be part of the type $p(\overline{x})$. Thus a realization of $p(\overline{x})$ might or might not satisfy $\phi (\overline{x})$.

Definition 2.1.

Let $T$ be a complete theory, $𝒜\vDash T$, and let $p(\overline{x})$ be a partial type. We say that a realization $\overline{a}$ of $p(\overline{x})$ in $𝒜$ is isolated if there is a formula $\phi (\overline{x})$ that isolates $p(\overline{x})$ and such that $𝒜\vDash \phi (\overline{a})$.

Theorem 2.2 (Omitting types).

Let $T$ be a complete theory, and let ${(p_i)}_{i\in \omega }$ be a countable list of partial types. There is a countable model $𝒜\vDash T$ such that any realization of any $p_i$ in $𝒜$ is isolated.

Proof.

We can construct $𝒜$ by the same construction as the standard type omitting argument except that we try to omit all of the types $p_i$ whether or not they are isolated. The result is that all realizations of any $p_i$ in $𝒜$ are isolated. ∎

The following lemma isolates the computability-theoretic content of the argument. It is more or less a standard application of computability-theoretic forcing with countable structures, which is essentially the same as the method of Vaught transforms.

Lemma 2.3.

Let $T$ be a relatively decidable theory. Then for all $𝒜\vDash T$ there is $\overline{a}\in 𝒜$ and a uniformly $T$-computable sequence of $T$-computable infinitary ${\mathrm{\Sigma }}_1$ formulas ${\mathrm{\Theta }}_{\phi }(\overline{x},\overline{y})$ such that for all $\phi$ we have

$$𝒜\vDash \phi (\overline{x})\leftrightarrow {\mathrm{\Theta }}_{\phi }(\overline{x},\overline{a}).$$

This condition is both sufficient and necessary, but it is a ${𝚷}_1^1$ condition on $T$ and will be superseded by the better characterization obtained in Theorem 1.2. Thus we prove only one direction.

Proof.

Suppose that $T$ is relatively decidable. Fix $𝒜\vDash T$. Following Montalbán [MON26] we can consider the elementary diagram of $𝒜$ as a relation on ,

$${\mathrm{Diag}}_{el}(𝒜)=\{(\mathrm{⌜}\phi \mathrm{⌝},\overline{a}):𝒜\vDash \phi (\overline{a})\}.$$

where $\mathrm{⌜}\phi \mathrm{⌝}$ is the Gödel number of $\phi$. Since $T$ is relatively decidable, the atomic diagram of $𝒜$ computes the elementary diagram of $𝒜$, and hence the elementary diagram of $𝒜$ is relatively intrinsically computable. By the Ash-Knight-Manasse-Slaman-Chisholm theorem [AKM+89, CHI90], in the version presented as Theorem II.16 in Montalbán’s book [MON21], there is $\overline{a}\in 𝒜$ and a uniformly computable sequence of computable ${\mathrm{\Sigma }}_1$ formulas ${\mathrm{\Theta }}_{\phi }(\overline{x},\overline{y})$ such that

$$𝒜\vDash \phi (\overline{x})⟷{\mathrm{\Theta }}_{\phi }(\overline{x},\overline{a}).\mathit{∎}$$

See 1.2

Proof.

For the easy direction, suppose that there is a formula $\phi (\overline{x})$ such that $T\vDash \exists \overline{x}\phi (\overline{x})$ and such that the $ℒ\cup \{\overline{c}\}$-theory $T\cup \{\phi (\overline{c})\}$ is model complete. Let $𝒜\vDash T$. Then there is some $\overline{a}\in 𝒜$ such that $𝒜\vDash \phi (\overline{a})$, and so $(𝒜,\overline{a})\vDash T\cup \{\phi (\overline{c})\}$. Since this theory is model complete, $T$ together with the atomic diagram of $(𝒜,\overline{a})$ computes the elementary diagram of this structure. Since $\overline{a}$ is a finite tuple of elements, the atomic and elementary diagrams of $(𝒜,\overline{a})$ are Turing equivalent to the atomic and elementary diagrams of $𝒜$ respectively.

Now suppose that $T$ is relatively decidable. Then by Lemma 2.3 for each $𝒜\vDash T$ there is $\overline{a}\in 𝒜$ and a uniformly computable sequence of computable ${\mathrm{\Sigma }}_1$ formulas ${\mathrm{\Theta }}_{\phi }(\overline{x},\overline{y})={\bigvee \bigvee }_{i=1}^{\mathrm{\infty }}{\theta }_{\phi ,i}(\overline{x},\overline{y})$, with each ${\theta }_{\phi ,i}(\overline{x},\overline{y})$ a finitary existential formula, such that for all $\phi$ we have

$$𝒜\vDash \forall \overline{x}[\phi (\overline{x})⟷\underset{i=1}{\overset{\mathrm{\infty }}{\bigvee \bigvee }}{\theta }_{\phi ,i}(\overline{x},\overline{a})].$$

Recall that these formulas came from a computability-theoretic forcing argument and that they are specific to the model $𝒜$. During the argument we will consider such formulas coming from two different models $ℬ$ and $𝒞$, and so we will use superscripts (e.g., ${\theta }_{\phi ,i}^{ℬ}(\overline{x},\overline{y})$) on these formulas to denote the associated model. The rest of the argument will be almost entirely model-theoretic (and though we use, e.g., recursive saturation, really all we need is countability rather than computability).

Now let $ℬ$ be a recursively saturated model of $T$. As in Lemma 2.3 let $\overline{b}\in ℬ$ and ${\mathrm{\Theta }}_{\phi }^{ℬ}(\overline{x},\overline{y})={\bigvee \bigvee }_{i=1}^{\mathrm{\infty }}{\theta }_{\phi ,i}^{ℬ}(\overline{x},\overline{y})$ be such that for all $\phi$,

$$ℬ\vDash \forall \overline{x}[\phi (\overline{x})⟷\underset{i=1}{\overset{\mathrm{\infty }}{\bigvee \bigvee }}{\theta }_{\phi ,i}^{ℬ}(\overline{x},\overline{b})].$$ (1)

We claim that for each $\phi$ there is $n_{\phi }$ such that

$$ℬ\vDash \forall \overline{x}[\phi (\overline{x})⟷\underset{i=1}{\overset{n_{\phi }}{\bigvee }}{\theta }_{\phi ,i}^{ℬ}(\overline{x},\overline{b})].$$

If not, then for some $\phi$ there is a sequence of tuples ${\overline{c}}_j$ with

$$ℬ\vDash \phi ({\overline{c}}_j)\wedge \underset{i=1}{\overset{j}{\bigwedge }}\neg {\theta }_{\phi ,i}^{ℬ}({\overline{c}}_j,\overline{b}).$$

Consider the partial type $q(\overline{x})=\{\phi (\overline{x}),\neg {\theta }_{\phi ,i}^{ℬ}(\overline{x},\overline{b}):i\in \omega \}$. This type is computable and finitely realizable in $ℬ$, and therefore as $ℬ$ is recursively saturated the type must be realized in $ℬ$. But by (1) no such type can be realized in $ℬ$. Thus we conclude that for each $\phi$ there is $n_{\phi }$ such that

$$ℬ\vDash \forall \overline{x}[\phi (\overline{x})⟷\underset{i=1}{\overset{n_{\phi }}{\bigvee }}{\theta }_{\phi ,i}^{ℬ}(\overline{x},\overline{b})].$$

In particular, for each $\phi$,

$$ℬ\vDash \exists \overline{y}\forall \overline{x}[\phi (\overline{x})⟷\underset{i=1}{\overset{n_{\phi }}{\bigvee }}{\theta }_{\phi ,i}^{ℬ}(\overline{x},\overline{y})].$$

Thus, as $T$ is complete, for each $\phi$ there is $n_{\phi }$ such that

$$T\vDash \exists \overline{y}\forall \overline{x}[\phi (\overline{x})⟷\underset{i=1}{\overset{n_{\phi }}{\bigvee }}{\theta }_{\phi ,i}^{ℬ}(\overline{x},\overline{y})].$$ (2)

Let ${\mathrm{\Theta }}_{e,\phi }(\overline{x},\overline{y})={\bigvee \bigvee }_{i=1}^{\mathrm{\infty }}{\theta }_{e,\phi ,i}(\overline{x},\overline{y})$ be a listing (indexed by $e$) of the computable sequences ${\{{\mathrm{\Theta }}_{e,\phi }(\overline{x},\overline{y})\}}_{\phi }$ (indexed by $\phi$) of computable ${\mathrm{\Sigma }}_1$ formulas. For each $e$, consider the partial type

$$p_e(\overline{y})=\{\forall \overline{x}\left({\theta }_{e,\phi ,i}(\overline{x},\overline{y})⟶\phi (\overline{x})\right):\phi ,i\}.$$

By the omitting types theorem there is a model $𝒞\vDash T$ such that any realization of any $p_e$ is isolated. As in Lemma 2.3 let $\overline{c}\in 𝒞$ and ${\mathrm{\Theta }}_{\phi }^{𝒞}(\overline{x},\overline{y})={\bigvee \bigvee }_{i=1}^{\mathrm{\infty }}{\theta }_{\phi ,i}^{𝒞}(\overline{x},\overline{y})$ be such that

$$𝒞\vDash \forall \overline{x}[\phi (\overline{x})⟷\underset{i=1}{\overset{\mathrm{\infty }}{\bigvee \bigvee }}{\theta }_{\phi ,i}^{𝒞}(\overline{x},\overline{c})].$$

Let $e$ be the index of the sequence ${\mathrm{\Theta }}_{\phi }^{𝒞}(\overline{x},\overline{y})$. Thus $\overline{c}$ realizes $p_e(\overline{y})$. This realization is isolated, say by a formula $\psi (\overline{y})$. In particular, for each formula $\phi$ and each $i$,

$$T\vDash \forall \overline{y}\left[\psi (\overline{y})⟶\forall \overline{x}\left({\theta }_{\phi ,i}^{𝒞}(\overline{x},\overline{y})⟶\phi (\overline{x})\right)\right].$$ (3)

Now by (2), for each $\phi$,

$$𝒞\vDash \exists \overline{y}\forall \overline{x}[\phi (\overline{x})⟷\underset{i=1}{\overset{n_{\phi }}{\bigvee }}{\theta }_{\phi ,i}^{ℬ}(\overline{x},\overline{y})].$$

Let ${\overline{d}}_{\phi }$ be this $\overline{y}$, and let

$${\chi }_{\phi }(\overline{y}):=\forall \overline{x}[\phi (\overline{x})⟷\underset{i=1}{\overset{n_{\phi }}{\bigvee }}{\theta }_{\phi ,i}^{ℬ}(\overline{x},\overline{y})].$$

Then since $𝒞\vDash {\chi }_{\phi }({\overline{d}}_{\phi })$, for some $i_{\phi }$ we have

$$𝒞\vDash {\theta }_{{\chi }_{\phi },i_{\phi }}^{𝒞}({\overline{d}}_{\phi },\overline{c}).$$

Thus, for each $\phi$,

$$T\vDash \exists \overline{x}\exists \overline{y}\left[\psi (\overline{y})\wedge {\theta }_{{\chi }_{\phi },i_{\phi }}^{𝒞}(\overline{x},\overline{y})\right]$$ (4)

and also, by (3),

$$T\vDash \forall \overline{x}\forall \overline{y}\left[\left(\psi (\overline{y})\wedge {\theta }_{{\chi }_{\phi },i_{\phi }}^{𝒞}(\overline{x},\overline{y})\right)⟶{\chi }_{\phi }(\overline{x})\right].$$ (5)

Recalling the definition of ${\chi }_{\phi }(\overline{x})$, this says that if we find $\overline{x},\overline{y}$ with $\psi (\overline{y})\wedge {\theta }_{{\chi }_{\phi },i_{\phi }}^{𝒞}(\overline{x},\overline{y})$ then, over the parameters $\overline{x}$, $\phi$ has a finitary existential definition $\phi (\overline{z})\leftrightarrow {\bigvee }_{i=1}^{n_{\phi }}{\theta }_{\phi ,i}^{ℬ}(\overline{z},\overline{x})$.

For simplicity in what follows, let

$${\nu }_{\phi }(\overline{x},\overline{y}):={\theta }_{{\chi }_{\phi },i_{\phi }}^{𝒞}(\overline{x},\overline{y})$$

and let

$${\eta }_{\phi }(\overline{z},\overline{x}):=\underset{i=1}{\overset{n_{\phi }}{\bigvee }}{\theta }_{\phi ,i}^{ℬ}(\overline{z},\overline{x}).$$

The important facts are that these are existential formulas and that, rewriting (4) and (5) in terms of this new notation,

$$T\vDash \exists \overline{x}\exists \overline{y}\left[\psi (\overline{y})\wedge {\nu }_{\phi }(\overline{x},\overline{y})\right]$$ (6)

and

$$T\vDash \forall \overline{x}\forall \overline{y}[(\psi (\overline{y})\wedge {\nu }_{\phi }(\overline{x},\overline{y}))⟶\forall \overline{z}(\phi (\overline{z})⟷{\eta }_{\phi }(\overline{z},\overline{x}))].$$ (7)

Otherwise, we can forget the specific forms that these formulas take. Note that this gives us for each $\phi$ a formula

$$\exists \overline{x}\exists \overline{y}\left[\psi (\overline{y})\wedge {\nu }_{\phi }(\overline{x},\overline{y})\wedge {\eta }_{\phi }(\overline{z},\overline{x})\right]$$

equivalent to $\phi (\overline{z})$ which would be existential if $\psi (\overline{y})$ were. This formula $\psi (\overline{y})$ is the same formula for all $\phi$, so we have essentially reduced to finding an existential formula equivalent to a single formula.

We now return to considering the recursively saturated model $ℬ$. Recall that there is $\overline{b}\in ℬ$ such that, for the formula $\psi (\overline{x})$ in particular,

$$ℬ\vDash \forall \overline{x}[\psi (\overline{x})⟷\underset{i=1}{\overset{\mathrm{\infty }}{\bigvee \bigvee }}{\theta }_{\psi ,i}^{ℬ}(\overline{x},\overline{b})].$$

As argued previously, since $ℬ$ is recursively saturated there is $n$ such that

$$ℬ\vDash \forall \overline{x}[\psi (\overline{x})⟷\underset{i=1}{\overset{n}{\bigvee }}{\theta }_{\psi ,i}^{ℬ}(\overline{x},\overline{b})].$$

Thus

$$ℬ\vDash \exists \overline{y}\forall \overline{x}[\psi (\overline{x})⟷\underset{i=1}{\overset{n}{\bigvee }}{\theta }_{\psi ,i}^{ℬ}(\overline{x},\overline{y})].$$

Let $\rho (\overline{x},\overline{y}):={\bigvee }_{i=1}^n{\theta }_{\psi ,i}^{ℬ}(\overline{x},\overline{y})$. Then, since $T$ is complete,

$$T\vDash \exists \overline{y}\forall \overline{x}[\psi (\overline{x})⟷\rho (\overline{x},\overline{y})].$$ (8)

We claim that the $ℒ\cup \{\overline{c}\}$-theory

$$T^{\ast }:=T\cup \{\forall \overline{x}[\psi (\overline{x})⟷\rho (\overline{x},\overline{c})]\}$$

is model complete. We will verify this by showing that for each formula $\phi$ we have

$$T^{\ast }\vDash \forall \overline{z}[\phi (\overline{z})⟷\exists \overline{x}\exists \overline{y}(\rho (\overline{y},\overline{c})\wedge {\nu }_{\phi }(\overline{x},\overline{y})\wedge {\eta }_{\phi }(\overline{z},\overline{x}))].$$ (9)

where $\exists \overline{x}\exists \overline{y}\left(\rho (\overline{y},\overline{c})\wedge {\nu }_{\phi }(\overline{x},\overline{y})\wedge {\eta }_{\phi }(\overline{z},\overline{x})\right)$ is an existential $ℒ\cup \{\overline{c}\}$ formula. Let $(𝒜,\overline{a})\vDash T^{\ast }$, that is, $𝒜\vDash T$ and

$$𝒜\vDash \forall \overline{x}[\psi (\overline{x})⟷\rho (\overline{x},\overline{a})].$$ (10)

Then for each formula $\phi$ we have, by (6) and (10),

$$𝒜\vDash \exists \overline{x}\exists \overline{y}\left[\rho (\overline{y},\overline{a})\wedge {\nu }_{\phi }(\overline{x},\overline{y})\right]$$ (11)

and, by (7) and (10),

$$𝒜\vDash \forall \overline{x}\forall \overline{y}[(\rho (\overline{y},\overline{a})\wedge {\nu }_{\phi }(\overline{x},\overline{y}))⟶\forall \overline{z}(\phi (\overline{z})⟷{\eta }_{\phi }(\overline{z},\overline{x}))].$$ (12)

Combining (11) and (12) we get

$$𝒜\vDash \forall \overline{z}[\phi (\overline{z})⟷\exists \overline{x}\exists \overline{y}(\rho (\overline{y},\overline{a})\wedge {\nu }_{\phi }(\overline{x},\overline{y})\wedge {\eta }_{\phi }(\overline{z},\overline{x}))].$$

This completes the proof of (9), and so we have shown that $T^{\ast }$ is model complete. Together with (8) we have completed the proof of the theorem. ∎

3 Marker extensions

Let $ℒ$ be a countable relational language. Let $T$ be an $ℒ$-theory and let ${\alpha }_1(\overline{x}),{\alpha }_2(\overline{x}),\mathrm{\dots }$ be a distinguished set of relations from $ℒ$ with ${\alpha }_i$ of arity $n_i$.

We will define a new language ${ℒ}^{+}$ and an ${ℒ}^{+}$-theory $T^{+}$ which we call the Marker extension of $T$ making ${\alpha }_1,{\alpha }_2,\mathrm{\dots }$ into ${\mathrm{\Sigma }}_1$ relations. This new theory will essentially be the same as the original theory $T$ except that the ${\alpha }_i(\overline{x})$ will be understood as definable ${\mathrm{\Sigma }}_1$ relations. Thus given some $𝒜\vDash T$, we can find some ${𝒜}^{+}\vDash T^{+}$ which is essentially the same, except we have now turned the ${\alpha }_i$ into ${\mathrm{\Sigma }}_1$-definable relations. Marker extensions, first introduced by Marker in [MAR89], are now a standard tool in computable structure theory, and there are many different ways of defining them with slightly different properties. While Marker used the construction at the level of a theory—which is what we will do—since then they have often been used on a single structure. We will give a full development in order to prove Lemma 3.2 which as far as we know is new.

Let our new language be

$${ℒ}^{+}=(ℒ-{\{{\alpha }_i(\overline{x})\}}_{i\in \omega })\cup {\{f_{i,j}(y)\}}_{i\in \omega ,1\le j\le n_i}\cup \{S_1(x),S_2(x)\}.$$

Here, $S_1$ and $S_2$ are unary relations, and the $f_{i,j}$ are unary functions. We will write $f_i(y)=\overline{x}$ for the function $f_i(y)=(f_{i,1}(y),\mathrm{\dots },f_{i,n_i}(y))$. At the level of formulas, $f_i(y)=\overline{x}$ stands for ${\bigwedge }_{j=1}^{n_i}{f}_{i,j}(y)=x_j$. Similarly we write $S_1(\overline{x})$ as shorthand for ${\bigwedge }_{i=1}^{\left|\overline{x}\right|}{S}_1(x_i)$.

We first explain, given an $ℒ$-structure $𝒜$, how to define its Marker extension ${𝒜}^{+}$ which will be an ${ℒ}^{+}$-structure. ${𝒜}^{+}$ will have two sorts. $S_1$ will identify the first sort, the elements from the original structure, and $S_2$ will identify the second sort, extra elements we add to our structure to certify whether a relation ${\alpha }_i$ is true or false. The domain of ${𝒜}^{+}$ will consist of the domain of $𝒜$, all satisfying the relation $S_1$, together with some number of new elements satisfying the relation $S_2$, and no other elements. (Usually we will have infinitely many new elements, but not always.) For each relation in $ℒ\cap {ℒ}^{+}$, we keep the relation the same on the domain of $𝒜$, and false on any other tuple. Then, for each ${\alpha }_i$ and $\overline{a}\in S_1$ such that $𝒜\vDash {\alpha }_i(\overline{a})$, we introduce an element $b$ of $S_2$ satisfying $f_i(b)=\overline{a}$. We say that $b$ witnesses that ${\alpha }_i(\overline{a})$ is true. Each element of $S_2$ will witness one and only one such relation. To fully define ${𝒜}^{+}$, we set $f_{i,j}(x)=x$ for $x$ from either sort if $x$ is not witnessing a relation ${\alpha }_i$. We have, in ${𝒜}^{+}$, definable relations ${\alpha }_i$ on the first sort which make the first sort isomorphic to $𝒜$. Thus $𝒜$ can be recovered from ${𝒜}^{+}$. We call ${𝒜}^{+}$ the Marker extension of $𝒜$ making ${\alpha }_1,{\alpha }_2,\mathrm{\dots }$ into ${\mathrm{\Sigma }}_1$ relations.

Given the theory $T$, we now define the theory $T^{+}$. Given $𝒜\vDash T$, we should have ${𝒜}^{+}\vDash T^{+}$. We begin with axioms for the sorts.

1. $T^{+}\vDash \forall x[S_1(x)\vee S_2(x)]$.

2. $T^{+}\vDash \forall x[S_1(x)⟷\neg S_2(x)]$.

For relation symbols $R$ from $ℒ$ which remain in ${ℒ}^{+}$, they can only be satisfied by tuples from the first sort.

1. $T^{+}\vDash \forall \overline{x}[R(\overline{x})⟶S_1(\overline{x})]$.

We now write down the axioms that ensure that the $f_{i,j}$ appropriately define relations on the first sort:

1. for all $i$ and $j=1,\mathrm{\dots },n_i$,

   $$T^{+}\vDash \forall x[S_1(x)⟶f_{i,j}(x)=x],$$

2. for all $i$,

   $$T^{+}\vDash \forall x\forall \overline{y}[[S_2(x)\wedge f_i(x)=\overline{y}]⟶[S_1(\overline{y})\vee \overline{y}=(x,\mathrm{\dots },x)]],$$

3. for all $i$,

   $$T^{+}\vDash \forall \overline{x}\forall y\forall z[[S_1(\overline{x})\wedge S_2(y)\wedge S_2(z)\wedge f_i(y)=\overline{x}\wedge f_i(z)=\overline{x}]⟶y=z],$$

4. for all $i\ne j$,

   $$T^{+}\vDash \forall \overline{x}\forall y[[S_1(\overline{x})\wedge S_2(y)\wedge f_i(y)=\overline{x}]⟶f_j(y)=(y,\mathrm{\dots },y)].$$

We now get ${\mathrm{\Sigma }}_1$-definable relations on tuples from the first sort corresponding to the ${\alpha }_i$. Abusing notation, we often also write ${\alpha }_i$ for these definable relations, but when we need to distinguish them we write ${\tilde{\alpha }}_i$.

$${\tilde{\alpha }}_i(\overline{x}):=\exists y[S_2(y)\wedge f_i(y)=\overline{x}]$$

When this holds, we say that $y$ is the witness to ${\alpha }_i(\overline{x})$. Axioms (6) ensure that each witness is unique, while axioms (7) ensure that each element cannot be a witness to two different relations ${\alpha }_i$ and ${\alpha }_j$. Since the $f_i$ are (tuples of) functions, each element cannot be a witness to two different relations for the same ${\alpha }_i$ on different tuples. We inductively define a transformation of an $ℒ$-formula $\phi$ into an ${ℒ}^{+}$-formula ${\phi }^{\ast }$ by replacing each instance of ${\alpha }_i$ with the definable relation ${\tilde{\alpha }}_i$, and with all variables of $\phi$ interpreted as belonging to $S_1$: Each quantifier $\exists \overline{x}\phi (\overline{x})$ becomes $\exists \overline{x}[S_1(\overline{x})\wedge {\phi }^{\ast }(\overline{x})]$, and each quantifier $\forall \overline{x}\phi (\overline{x})$ becomes $\forall \overline{x}[S_1(\overline{x})⟶{\phi }^{\ast }(\overline{x})]$. If $\phi (\overline{x})$ has free variables $\overline{x}$, in ${\phi }^{\ast }(\overline{x})$ we also assert that $\overline{x}\in S_1$. For the final axioms of $T^{+}$, we take the axioms of $T$, translated as just described.

1. $T^{+}\vDash {\phi }^{\ast }$ for each $\phi \in T$.

This completes the definition of $T^{+}$.

We begin with some observations. If $T$ is consistent, say with a model $𝒜$, then ${𝒜}^{+}$ is a model of $T^{+}$. Thus:

Lemma 3.1.

If $T$ is consistent, then $T^{+}$ is consistent.

On the other hand, given a model $ℳ$ of $T^{+}$, we can define an associated model $𝒜$ whose domain is the first sort of $ℳ$, and interprets the ${\alpha }_i$ using the definable relations ${\tilde{\alpha }}_i$. Axioms (8) ensure that $𝒜\vDash T$. It is not necessarily true that $ℳ$ is ${𝒜}^{+}$, but ${𝒜}^{+}$ will be a substructure of $ℳ$, with $ℳ-{𝒜}^{+}$ consisting only of elements of the second sort $S_2$ which are not witnesses to any relations. For $n\in \omega \cup \{\omega \}$, we write ${𝒜}_n^{+}$ for the structure which is ${𝒜}^{+}$ together with $n$ additional elements in the second sort which are not witnesses to any relations. The ${𝒜}_n^{+}$ for $n\ge 1$ may not be models of $T^{+}$ in all cases, but often by compactness they will be. One such instance is if $T$ satisfies a technical assumption we call ($\ast$): $T\vDash \exists \overline{x}{\alpha }_i(\overline{x})$ for infinitely many $i$. In this case the countable models of $T^{+}$ are exactly the models ${𝒜}_n^{+}$ for $𝒜\vDash T$ and $n\in \omega \cup \{\omega \}$.

Next, we prove the following quantifier-elimination result which says that any ${ℒ}^{+}$ formula about a model of $T^{+}$ can be expressed by a Boolean combination of quantifier-free ${ℒ}^{+}$-formulas and formulas (possibly involving quantifiers) in the original language $ℒ$ which have been translated to ${ℒ}^{+}$. For this we will need to assume that $T$ satisfies ($\ast$).

Lemma 3.2.

Suppose that $T$ has property ($\ast$). Then $T^{+}$ has quantifier elimination in the language

$${ℒ}^{\ast }={ℒ}^{+}\cup \{{\phi }^{\ast }:\phi \text{ an }ℒ\text{-formula}\}.$$

Sometimes one always allows at least one free variable in a quantifier elimination result. Here we do not: every sentence is equivalent to a quantifier-free sentence. This yields the following important lemma which we state and prove before returning to the proof of the proposition.

Lemma 3.3.

If $T$ is complete and has property ($\ast$), then $T^{+}$ is complete.

Proof.

Given an ${ℒ}^{+}$-sentence $\theta$, we can write $\theta$ as a Boolean combination of atomic and negated atomic formulas from

$${ℒ}^{+}\cup \{{\phi }^{\ast }:\phi \text{ an }ℒ\text{-formula}\}$$

with no free variables. The only atomic formulas with no free variables are the ${\phi }^{\ast }$ for $\phi$ an $ℒ$-sentence. But since $T$ decides each such sentence $\phi$, $T^{+}$ decides each such ${\phi }^{\ast }$. ∎

We now return to prove Lemma 3.2.

Proof of Lemma 3.2.

Using the standard criterion for proving quantifier elimination, it suffices to prove the following. Let $𝒜$ be an ${ℒ}^{\ast }$-structure and $ℳ,𝒩\vDash T^{+}$. Suppose that $𝒜\subseteq ℳ$ and $𝒜\subseteq 𝒩$ as ${ℒ}^{\ast }$-structures. Let $\phi (\overline{x},y)$ be a quantifier-free ${ℒ}^{\ast }$-formula. Let $\overline{a}\in 𝒜$ and $u\in ℳ$ and suppose that $ℳ\vDash \phi (\overline{a},u)$. We must show that there is $v\in 𝒩$ such that $𝒩\vDash \phi (\overline{a},v)$. We may assume that $u\notin 𝒜$, or we would already be done.

We begin by making some simplifications. After writing $\phi$ in disjunctive normal form, one of the disjuncts must be true in $ℳ$ and so we can replace $\phi$ by this disjunct. Thus we assume that $\phi$ is a conjunction of atomic and negated atomic formulas. We may also assume that $\phi$ has at most one conjunct of the form ${\psi }^{\ast }$, as a conjunction ${\psi }_1^{\ast }\wedge {\psi }_2^{\ast }$ is equivalent to ${({\psi }_1\wedge {\psi }_2)}^{\ast }$. This includes any of the relations $R$ from $ℒ-\{{\alpha }_1,{\alpha }_2,\mathrm{\dots }\}$ as for such relations $R$ and $R^{\ast }$ are equivalent. Then we can write

$$\phi (\overline{a},u)\equiv {\psi }^{\ast }(\overline{s}(\overline{a},u))\wedge \mathrm{\cdots }$$

where $\overline{s}$ is a tuple of terms with $\overline{s}(\overline{a},u)$ in $S_1$ and $\mathrm{\cdots }$ is a conjunction of equalities, inequalities, and relations $S_1$ and $S_2$ of terms in $\overline{a},u$. Note that all of the functions in the language are unary, and so all terms are unary, and in particular, no term can involve both part of $\overline{a}$ and $u$. We can also rewrite $\overline{a}$ as $\overline{a},\overline{b}$ where $\overline{a}$ is in the first sort and $\overline{b}$ is in the second sort. We can also expand $\overline{a}$ to include all of the images of $\overline{b}$ under any terms (other than those that map $b_i$ to itself), as each element of $S_2$ has only finitely many images under terms, and each term maps an element either to itself or to $S_1$. After this, we may rewrite our formula as

$$\phi (\overline{a},\overline{b},u)\equiv {\psi }^{\ast }(\overline{a},s_1(u),\mathrm{\dots },s_n(u))\wedge \mathrm{\cdots }$$

where $s_1,\mathrm{\dots },s_n$ are terms with $s_i(u)\in S_1$ and the other conjuncts are as before.

Now we make some simplifications involving the other conjuncts. Any atomic formula only involving $\overline{a}$ is passed to $𝒩$ trivially, so we can ignore these. Since $S_1$ is equivalent to $\neg S_2$, and vice versa, we may assume that they appear only positively. Since the only function symbols in the language are unary, each term has only a single variable. Any term applied to one of the $a_i$ must be $a_i$. Also, for any term $t$ and any $i$ either $t(b_i)=b_i$ or there is $j$ such that $t(b_i)=a_j$. Thus remaining atomic formulas involving $u$ are:

• $a_i=t(u)$ or $b_i=t(u)$

• $a_i\ne t(u)$ or $b_i\ne t(u)$

• $t_1(u)=t_2(u)$

• $t_1(u)\ne t_2(u)$

• $t(u)\in S_1$,

• $t(u)\in S_2$.

We also make several remarks about terms. Given $ℳ\vDash T^{+}$, $x\in ℳ$, and any term $t$:

1. Either $ℳ\vDash t(x)\in S_1$ or $ℳ\vDash t(x)=x$.

2. If $ℳ\vDash x\in S_1$ then $t(x)=x$.

We will use these implicitly.

We now split into cases according to whether $u\in S_1$ or $u\in S_2$, and in the latter case into subcases depending on whether $u$ is a witness to some ${\alpha }_k$ or not. In each case we find $v\in 𝒩$ which fits into the same case (e.g., $ℳ\vDash u\in S_1$ if and only if $𝒩\vDash v\in S_1$).

Case 1: $u\in S_1$.

Since $u\in S_1$, $t(u)=u$ for any term $t$. This simplifies all of the atomic and negated atomic formulas in the conjunction. Any equalities and inequalities between $u$ and $\overline{a}$ can be moved into $\psi$, and we cannot have any equalities between $u$ and $\overline{b}$. Also, $u\in S_1$ and $u\notin S_2$. As we will choose $v\in S_1$, all of these remaining atomic and negated atomic formulas will hold. Thus, as long as we pick $v$ in $𝒩$ with $v\in S_1$ and such that $𝒩\vDash {\psi }^{\ast }(\overline{a},v)$ then we are done.

We have

$$ℳ\vDash {\psi }^{\ast }(\overline{a},u)⟹ℳ\vDash \exists y{\psi }^{\ast }(\overline{a},y)⟺ℳ\vDash {(\exists y\psi (\overline{x},y))}^{\ast }(\overline{a})$$

Since the latter formula is quantifier-free, we have that

$$ℳ\vDash {(\exists y\psi (\overline{x},y))}^{\ast }(\overline{a})⟹𝒩\vDash {(\exists y\psi (\overline{x},y))}^{\ast }(\overline{a})⟹𝒩\vDash \exists y{\psi }^{\ast }(\overline{a},y)$$

Thus there is some $v\in 𝒩$ such that $𝒩\vDash {\psi }^{\ast }(\overline{a},v)$. This implies that $v\in S_1$.

Case 2: $u\in S_2$, $u$ is a witness to ${\alpha }_k(\overline{c})$ for $\overline{c}\in ℳ$.

By saying that $u$ is a witness to ${\alpha }_k(\overline{c})$ in $ℳ$ we mean that $f_k(u)=\overline{c}$. We begin by splitting $\overline{c}$ into part that is in $\overline{a}$ and part that is not. After rearranging, we may replace $\overline{c}$ by $({\overline{a}}^{\prime },\overline{c})$ where ${\overline{a}}^{\prime }=(a_{i_1},\mathrm{\dots },a_{i_p})$ is a subtuple of $\overline{a}$ and $\overline{c}=(c_1,\mathrm{\dots },c_q)$ has no entries in common with $\overline{a}$. Also, the only terms $s(u)$ are (up to equivalence, when applied to $u$) the identity and $s=f_{k,m}$ for each $m$. Rearranging the $\{f_{k,1},\mathrm{\dots },f_{k,n_k}\}$ we may assume that $f_{k,m}(u)=a_{i_m}$ for $1\le m\le p$ and $f_{k,p+m}(u)=c_m$ for $1\le m\le q$. Moreover, for any $v$ in $S_2$, as long as $f_{k,m}(v)\in S_1$ for some $m$, then the terms $s(v)$ up to equivalence are the same. So we may rewrite our formula as

$$\phi (\overline{a},\overline{b},u)\equiv {\psi }^{\ast }(\overline{a},\overline{c})\wedge \underset{1\le m\le p}{\bigwedge }{f}_{k,m}(u)=a_{i_m}\wedge \underset{1\le m\le q}{\bigwedge }{f}_{k,p+m}(u)=c_m\wedge \mathrm{\cdots }.$$

Thus we have

$$ℳ\vDash {\tilde{\alpha }}_k({\overline{a}}^{\prime },\overline{c})\wedge {\psi }^{\ast }(\overline{a},\overline{c})\wedge \mathrm{\Delta }(\overline{a},\overline{c})$$

where $\mathrm{\Delta }$ is the formula that expresses the equalities and inequalities between all elements of $\overline{a}$ and $\overline{c}$, including that $a_i\ne c_j$ for all $i,j$. Thus

$$ℳ\vDash \exists \overline{y}[{\tilde{\alpha }}_k({\overline{a}}^{\prime },\overline{y})\wedge {\psi }^{\ast }(\overline{a},\overline{y})\wedge \mathrm{\Delta }(\overline{a},\overline{y})].$$

We can rewrite this as

$$ℳ\vDash {(\exists \overline{y}[{\alpha }_k({\overline{x}}^{\prime },\overline{y})\wedge \psi (\overline{x},\overline{y})\wedge \mathrm{\Delta }(\overline{x},\overline{y})])}^{\ast }(\overline{a})$$

where ${\overline{x}}^{\prime }=(x_{i_1},\mathrm{\dots },x_{i_p})$. Since this is a quantifier-free fact about $\overline{a}\in 𝒜$, it is also true in $𝒩$,

$$𝒩\vDash {(\exists \overline{y}[{\alpha }_k({\overline{x}}^{\prime },\overline{y})\wedge \psi (\overline{x},\overline{y})\wedge \mathrm{\Delta }(\overline{x},\overline{y})])}^{\ast }(\overline{a}).$$

Thus

$$𝒩\vDash \exists \overline{y}[{\alpha }_k({\overline{a}}^{\prime },\overline{y})\wedge {\psi }^{\ast }(\overline{a},\overline{y})\wedge \mathrm{\Delta }(\overline{a},\overline{y})].$$

Letting $\overline{d}\in 𝒩$ be the witness to this existential quantifier over $\overline{y}$, we have

$$𝒩\vDash {\tilde{\alpha }}_k({\overline{a}}^{\prime },\overline{d})\wedge {\psi }^{\ast }(\overline{a},\overline{d})\wedge \mathrm{\Delta }(\overline{a},\overline{d}).$$

Note that the $d_i$ are distinct from the $a_j$ and $c_i=c_j$ if and only if $d_i=d_j$.

We also have $𝒩\vDash {\tilde{\alpha }}_k({\overline{a}}^{\prime },\overline{d})$. Let $v\in 𝒩$ be the witness to this, i.e., the unique element such that $f_k(v)=({\overline{a}}^{\prime },\overline{d})$. So we have

$$𝒩\vDash \underset{1\le m\le p}{\bigwedge }{f}_{k,m}(v)=a_{i_m}\wedge \underset{1\le m\le q}{\bigwedge }{f}_{k,p+m}(v)=d_m.$$

We also have that $v\notin \overline{b}$, argued as follows. In that case, we would have $v\in 𝒜$ and so $v\in ℳ$. By our assumption that $\overline{a}$ contains the non-trivial images of $\overline{b}$ under all terms, we would have that $\overline{c}$ and $\overline{d}$ are the empty tuple. But ${\alpha }_k({\overline{a}}^{\prime })$ can have only one witness in $ℳ$, and both $u$ and $v$ would be witnesses. This contradicts our assumption that $u\notin 𝒜$.

Now we must consider all of the other conjuncts in our formula and use the fact that they were true for $u$ to show that they are true for $v$. It will be useful to note that for any term $t$, $t(u)=u$ if and only if $t(v)=v$, and otherwise there is some $m$ such that $t(u)=f_{k,m}(u)$ and $t(v)=f_{k,m}(v)$. Thus $t(u)=a_i$ if and only if $t(v)=a_i$, and $t(u)=c_i$ if and only if $t(v)=d_i$.

• Given $a_i=t(u)$ for some term $t$, we must have that $t(u)=f_{k,m}(u)$ for some $m$ as otherwise $t(u)$ would not be in $S_1$. Thus $a_i=a_{i_m}=f_{k,m}(v)=t(v)$.

• Given $b_i=t(u)$, since $u$ and $b_i$ are in $S_2$, we must have $b_i=u$. But this contradicts our assumption that $u\notin 𝒜$.

• Given $a_i\ne t(u)$, one of the following must be true:

  • $t(u)=u$ and $t(v)=v\ne a_i$.

  • $t(u)=f_{k,p+m}(u)=c_m$ for some $1\le m\le q$. Then $t(v)=f_{k,p+m}(v)=d_m$ and $d_m\ne a_i$.

  • $t(u)=f_{k,m}(u)=a_{i_m}$ for some $1\le m\le p$, and $a_{i_m}\ne a_i$. Then $t(v)=f_{k,m}(v)=a_{i_m}\ne a_i$.

• Given $b_i\ne t(u)$ for some term, we have that either $t(v)\in S_1$ or $t(v)=v$. In the former case, we automatically have that $b_i\ne t(v)$. In the latter case, we have two subcases. If $\overline{d}$ is a non-empty tuple, then since $\overline{d}$ does not share elements with $\overline{a}$ and is generated by $v$, $v\ne b_i$, since $b_i$ can only generate itself and elements of $\overline{a}$. If $\overline{d}$ is empty, then so is $\overline{c}$. If $\overline{c}$ is empty, then $u$ is the unique witness in $ℳ$ to ${\alpha }_k({\overline{a}}^{\prime })$, and so $b_i$ is not a witness to ${\alpha }_k({\overline{a}}^{\prime })$. Since $v$ is the unique witness in $𝒩$ to ${\alpha }_k({\overline{a}}^{\prime })$, $b_i\ne v$.

• Given $t_1(u)=t_2(u)$ (or $t_1(u)\ne t_2(u)$), since terms behave essentially the same on $v$ as they do on $u$, (including that, e.g., $c_i=c_j$ if and only if $d_i=d_j$) we also have $t_1(v)=t_2(v)$ (or $t_1(v)\ne t_2(v)$).

• Given $t(u)\in S_1$ we must have $t(u)=f_{k,m}(u)$ and so $t(v)=f_{k,m}(v)$ is also in $S_1$.

• Given $t(u)\in S_2$ we must have $t(u)=u$, and so $t(v)=v$ is also in $S_2$.

Thus we have shown that $𝒩\vDash \phi (\overline{a},\overline{b},v)$.

Case 3: $u\in S_2$, $u$ is not a witness to any ${\alpha }_k$.

For every term $t$, $t(u)=u$ is in $S_2$. Thus we may rewrite

$$\phi (\overline{a},\overline{b},u)\equiv {\psi }^{\ast }(\overline{a})\wedge \mathrm{\cdots }$$

and since ${\psi }^{\ast }(\overline{a})$ depends only on elements in $𝒜$ and hence is automatically true in $𝒩$, we may remove it and assume that $\phi (\overline{a},\overline{b},u)$ is a conjunction of atomic and negated atomic formulas of the types described above.

Since, by assumption, $u$ is not part of the tuple $\overline{b}$, and is not a witness, we can remove the equalities of the form $a_i=t(u)$. Since in $ℳ$ for every term $t$ we have $t(u)=u$, no inequalities $t_1(u)\ne t_2(u)$ can be true in $ℳ$, and so we can discard those as a possibility. We can also replace any equalities $t_1(u)=t_2(u)$ with two equalities of the form $t(u)=u$. Finally, since $t(u)=u$ is in $S_2$ in $ℳ$, we can discard atomic formulas $t(u)\in S_1$. We are left with the following:

• $a_i\ne t(u)$ or $b_i\ne t(u)$

• $t(u)=u$

• $t(u)\in S_2$.

Let $K$ be the maximum of the $k$ such that some $f_{k,i}$ shows up in one of the terms $t$ in our formula, and also so that any $b_i\in \overline{b}$ is a witness to some ${\alpha }_k$. It will suffice to choose $v$ to be a witness to some ${\alpha }_m$ for some $m>K$, and that such an element exists by assumption ($\ast$)—the original theory $T$ was assumed to contain elements that witness ${\alpha }_m$ for arbitrarily large $m$. In this case, for all terms $t$ appearing in our formula, we have $t(v)=v$. Also, $v\in S_2$, and $v$ does not appear among the $\overline{b}$, and so we are done.

This completes the three cases. We have proved quantifier elimination down to ${ℒ}^{\ast }$. ∎

The intention when taking a Marker extension is that given $𝒜$ an $ℒ$-structure we should be able to treat the relations ${\alpha }_i$ as being existential. If an existential formula is true in a substructure, it is true in a superstructure; but it may be false in a substructure and yet true in a superstructure. We define a new notion of substructure, which we call a weak substructure, to take this into account.

Definition 3.4.

Let $𝒜$ and $ℬ$ be $ℒ$-structures. We say $𝒜$ is a weak substructure of $ℬ$, denoted as $𝒜{\subseteq }_wℬ$ if

1. The domain of $𝒜$ is contained in the domain of $ℬ$;

2. if $𝒜\vDash {\alpha }_i(\overline{a})$ for $\overline{a}\in 𝒜$, then $ℬ\vDash {\alpha }_i(\overline{a})$; and

3. for any other relation $R\in ℒ-\{{\alpha }_1,{\alpha }_2,\mathrm{\dots }\}$ and $\overline{a}\in 𝒜$, $𝒜\vDash R(\overline{a})$ if and only if $ℬ\vDash R(\overline{a})$.

By taking Marker extensions, we can realize weak substructures as true substructures.

Lemma 3.5.

If $𝒜{\subseteq }_wℬ$ then ${𝒜}^{+}\subseteq {ℬ}^{+}$.

Proof.

Supposing that $𝒜$ is a weak substructure of $ℬ$, we must define an embedding of ${𝒜}^{+}$ into ${ℬ}^{+}$. The embedding is defined as follows. On the first sort $S_1$, we just have the embedding $𝒜\to ℬ$ as these make up the first sorts of ${𝒜}^{+}$ and ${ℬ}^{+}$ respectively. On the second sort $S_2$, any element $c$ of ${𝒜}^{+}$ is a witness that ${\alpha }_i$ holds of some tuple $\overline{a}\in 𝒜$. Since $𝒜$ is a weak substructure of $ℬ$, ${\alpha }_i$ also holds of $\overline{a}$ in $ℬ$, and so there is a witness $d$ to this in ${ℬ}^{+}$. We map $c$ to $d$. Each $c$ witnesses ${\alpha }_i(\overline{a})$ for exactly one pair $i$ and $\overline{a}$, and there is only one witness $d$ to the same pair in ${ℬ}^{+}$. Thus this map ${𝒜}^{+}\to {ℬ}^{+}$ is uniquely defined and injective. It is also not hard to see that it is an ${ℒ}^{+}$-embedding. ∎

The previous lemma also, of course, applies when $𝒜\subseteq ℬ$ is a true substructure.

Lemma 3.6.

Let $S\vDash T$ as $ℒ$-theories. Then $S^{+}\vDash T^{+}$ as ${ℒ}^{+}$-theories.

Proof.

Axioms ($1$) and ($2$) are common to the Marker extension of any theory. Axioms ($3$)-($7$) are satisfied by both $S^{+}$ and $T^{+}$ since those axioms only depend on $ℒ$ and set $\{{\alpha }_1,{\alpha }_2,\mathrm{\dots }\}$ of relations to be made existential. Consider an instance of Axiom $(8)$, say $S^{+}\vDash {\phi }^{\ast }$ where $S\vDash \phi$. Since $S\vDash T$, $T\vDash \phi$ and so $T^{+}\vDash {\phi }^{\ast }$ as an instance of Axiom ($8$). ∎

4 Incomplete theories

In this section we will prove the anti-classification result for incomplete theories.

See 1.3

Proof.

Given a tree we may assume, without changing whether or not $𝔗$ is well-founded, that each non-leaf node $\sigma \in 𝔗$ has all of its possible children $\sigma i$ in $𝔗$. Uniformly computably in $𝔗$ we will define a language $ℒ={ℒ}_{𝔗}$ and an (incomplete) theory $T=T_{𝔗}$ such that $𝔗$ is well-founded if and only if $T_{𝔗}$ is relatively decidable. Thus the set

$$\{(ℒ,T):\text{the }ℒ\text{-theory }T\text{ is relatively decidable}\}$$

will be ${𝚷}_1^1$-Wadge-complete. One can see from the construction below that the language always consists of the same number of symbols of the same arities, and so we could make the construction with a fixed language. Indeed, following [BH19] we conjecture that one could take the language $ℒ$ to be finite.

Fix a tree $𝔗$ with the property that each non-leaf node has all of its children. Let

$$ℒ=\{U_{\sigma }(x):\sigma \in 𝔗\}\cup \{A_i(x):i\in \omega \}\cup \{V_{i,\sigma }(\overline{y},x):i\in \omega ,\sigma \in 𝔗\}.$$

For each $k$ let

The $U_{\sigma }$ and $A_i$ are unary relations. The arities of the $V_{i,\sigma }$ must be defined inductively. Enumerate the universal $ℒ$-formulas as $P_i(\overline{x})$ with $P_i(\overline{x})$ an ${ℒ}_i$-formula. Thus $P_i(\overline{x})$ does not involve any of the symbols $V_{i,\sigma }$. Then we may construct $ℒ$ so that the arity of $\overline{y}$ in $V_{i,\sigma }(\overline{y},x)$ is the same as in $P_i(\overline{y},x)$. Let $T$ be the theory with the following axioms:

1. $\exists x{U}_{\mathrm{\varnothing }}(x)$,

2. for $\sigma \in 𝔗$ a non-leaf node,

   $$[U_{\sigma }(x)\wedge \underset{j=0}{\overset{i}{\bigwedge }}\forall y\neg U_{\sigma j}(y)]⟶\forall \overline{y}[P_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)],$$

3. for $\tau \in 𝔗$ a leaf node,

   $$U_{\tau }(x)⟶\forall \overline{y}[P_i(\overline{y})⟷V_{i,\tau }(\overline{y},x)].$$

We begin by showing that $T$ is satisfiable.

Lemma 4.1.

$T$ is satisfiable and has an infinite model.

Proof.

We will define a model $𝒜\vDash T$ on an infinite domain. Set $U_{\mathrm{\varnothing }}(x)$ for all $x\in 𝒜$ and $\neg U_{\sigma }(x)$ for all $x\in 𝒜$ and all $\sigma \in 𝔗$, $\sigma \ne \mathrm{\varnothing }$. This ensures that axiom (1) is true. We set $A_i(x)$ to be true for all $i$ and all $x\in 𝒜$.

We will define the $V_{i,\sigma }$ such that for all $x\in 𝒜$,

$$𝒜\vDash \forall \overline{y}[P_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)].$$

This will ensure that the axioms of types (2) and (3) are all true. Because the symbols $V$ are included in the formulas $P$, we must define the $V$’s recursively. We begin with $P_0$ which uses only $U_{\mathrm{\varnothing }}$ and the symbol for equality, so that we have already determined whether $𝒜\vDash P_0(\overline{y})$ for each $\overline{y}$. We can thus set, for each $\overline{y}$ and $x$, $𝒜\vDash V_{0,\sigma }(\overline{y},x)$ if and only if $𝒜\vDash P_0(\overline{y})$. Now supposing that we have defined the $V_{i,\sigma }$ for , we define the $V_{k,\sigma }$. We have already at this point determined whether $𝒜\vDash P_k(\overline{y})$ for each $\overline{y}$, and so can again set $𝒜\vDash V_{k,\sigma }(\overline{y},x)$ if and only if $𝒜\vDash P_k(\overline{y})$. ∎

Now let $T^{+}$ be the Marker extension of $T$ where we make each $A_i$ and $U_{\sigma }$ universal (i.e., we make each of their negations existential). Since $T$ is consistent, so is $T^{+}$. We will now argue that $T^{+}$ is relatively decidable if and only if $𝔗$ is well-founded.

Lemma 4.2.

Suppose that $𝔗$ is well-founded. Then $T^{+}$ is relatively decidable.

Proof.

Let ${𝒜}^{+}\vDash T^{+}$ and let $𝒜$ be the corresponding model of $T$. We have that $𝒜\vDash \exists x{U}_{\mathrm{\varnothing }}(x)$. Since the tree $𝔗$ is well-founded, there must either be some $\sigma \in 𝔗$ a non-leaf node such that $𝒜\vDash \exists x{U}_{\sigma }(x)$ and for each $k$, $𝒜\vDash \forall x\neg U_{\sigma k}(x)$, or some $\tau \in 𝔗$ a leaf node such that $𝒜\vDash \exists x{U}_{\tau }(x)$.

In the first case, let $c$ be such that $𝒜\vDash U_{\sigma }(c)$. Then, following axioms (2), we have for all $i$ that

$$𝒜\vDash \forall \overline{y}[P_i(\overline{y})⟷V_{i,\sigma }(\overline{y},c)].$$

In the second case, let $c$ be such that $𝒜\vDash U_{\tau }(c)$. Then, following the axioms (3), we also have that for all $i$

$$𝒜\vDash \forall \overline{y}[P_i(\overline{y})⟷V_{i,\tau }(\overline{y},c)].$$

From here the argument is the same in both cases. In any computations below, we fix the element $c$ and $\sigma$ (or $\tau$, but below we will write $\sigma$) non-uniformly.

Each universal $ℒ$-formula is equivalent to a quantifier-free $ℒ$-formula $V_{i,\sigma }(\overline{y},c)$ with parameter $c$. We can argue inductively that this implies that each $ℒ$-formula $\phi (\overline{y})$ is equivalent to an $ℒ$-formula $V_{i_{\phi },\sigma }(\overline{y},c)$. (With $\phi (\overline{y})$ in normal form, work from the inside out replacing each universal formula by some $V_{i,\sigma }$ and each existential formula by some $\neg V_{i,\sigma }$.) Using $T^{+}$ (which is Turing-equivalent to $T$) for each $\phi$ we can compute such an $i_{\phi }$.

Given an ${ℒ}^{+}$-formula $Q(\overline{y})$, by Lemma 3.2 there is an equivalent quantifier-free formula $P(\overline{y})$ in the language ${ℒ}^{+}\cup \{{\phi }^{\ast }:\phi \text{ an }ℒ\text{-formula}\}$. Using $T$, we can compute such a formula. Each ${\phi }^{\ast }(\overline{y})$ is equivalent in ${𝒜}^{+}$ to the ${ℒ}^{+}$-formula $V_{i_{\phi },\sigma }^{\ast }(\overline{y},c)$, which is the same as $V_{i_{\phi },\sigma }(\overline{y},c)$ as they were not made universal in the Marker extension. Thus $Q(\overline{y})$ is equivalent in ${𝒜}^{+}$ to a quantifier-free ${ℒ}^{+}$-formula with parameter $c$. Thus the atomic diagram of ${𝒜}^{+}$, together with $T$, can compute the elementary diagram of ${𝒜}^{+}$. ∎

The more difficult case is the case that $𝔗$ is ill-founded. In this case, we will show that there is a complete theory $S^{+}$ extending $T^{+}$ which is not relatively decidable. This will imply that $T^{+}$ is not relatively decidable. The advantage of finding a completion of $T^{+}$ is that we can apply our characterization for when a complete theory is relatively decidable. We will apply one direction of that characterization, which is that we will show that there is no formula $\phi (\overline{x})$ such that

• $S^{+}\vDash \exists \overline{x}\phi (\overline{x})$, and

• the ${ℒ}^{+}\cup \{\overline{c}\}$-theory $S^{+}\cup \{\phi (\overline{c})\}$ is model complete.

The theory $S^{+}$ will be defined from a fixed path through $𝔗$.

Instead of directly finding a completion of $T^{+}$, we will first find a completion of $T$ and then take its Marker extension, which is justified by Lemma 3.6. Suppose that $𝔗$ has an infinite path $\pi$. Let $T_{\pi }$ be the theory with the following axioms.

1. for each $\sigma \nprec \pi$,

   $$\neg \exists x{U}_{\sigma }(x)$$

2. for each $\sigma \prec \pi$, with $\mathrm{\ell }$ such that $\sigma \mathrm{\ell }\prec \pi$, and ,

   $$U_{\sigma }(x)⟶\forall \overline{y}[P_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)].$$

Note that $T_{\pi }\cup \{\exists x{U}_{\sigma }(x):\sigma \prec \pi \}\vDash T$. Thus to find a completion of $T$ it suffices to find a completion of $T_{\pi }\cup \{\exists x{U}_{\sigma }(x):\sigma \prec \pi \}$.

We could attempt to take a model completion of $T_{\pi }$, which is a ${\forall }_2$ theory, but to do this we would have to show that the existentially closed models of $T_{\pi }$ are an elementary class. This is not straightforward and we are not sure if this is true. (The difficulty stems from the fact that the $P_i$ range over all universal formulas.) Instead, we will construct a completion of $T_{\pi }$ by Fraïssé limits. The language $ℒ$ is infinite, so rather than trying to take a Fraïssé limit of $T_{\pi }$ itself, we will find a completion of $T_{\pi }$ which is a union of Fraïssé limits. And since $T_{\pi }$ is not a universal theory we cannot simply take the Fraïssé limits of $T_{\pi }$ restricted to finite languages, but must instead do something more complicated.

We recall some definitions from Fraïssé theory. We work purely in the case where $ℒ$ is a finite relational language. Recall that the age of an $ℒ$-structure $𝒜$ is the set $\mathrm{Age}(𝒜)$ of all finite substructures of $𝒜$. Given $𝕂$ a class of (isomorphism types) of finite structures, we say that $𝕂$ is a Fraïssé class if it has the Hereditary Property (HP), Amalgamation Property (AP), and the Joint Embedding Property (JEP). Then there is a unique countable homogeneous structure, called the Fraïssé limit of $𝕂$, whose age is $𝕂$. We write $\mathrm{Flim}(𝕂)$ for the Fraïssé limit of the class $𝕂$. Since we assume that the language was finite and relational, $\mathrm{Age}(𝕂)$ is automatically uniformly locally finite and hence the theory of the Fraïssé limit is $\omega$-categorical and admits quantifier elimination. Given a universal theory $T$ we have the corresponding class $𝕂(T)$ of finite models of $T$. $𝕂(T)$ automatically has the HP.

Given two Fraïssé classes ${𝕂}_1$ and ${𝕂}_2$ in languages ${ℒ}_1$ and ${ℒ}_2$ respectively, we say that ${𝕂}_2$ is an expansion class of ${𝕂}_1$ if ${𝕂}_1={𝕂}_2{\mathrm{\upharpoonright }}_{{ℒ}_1}:=\{𝒜{\mathrm{\upharpoonright }}_{{ℒ}_1}|𝒜\in {𝕂}_2\}$, the class of reducts of structures in ${𝕂}_2$. If ${𝕂}_2$ is an expansion class of ${𝕂}_1$ we say that the pair $({𝕂}_1,{𝕂}_2)$ is reasonable if whenever ${𝒜}_2\in {𝕂}_2$, ${𝒜}_1={𝒜}_2{\mathrm{\upharpoonright }}_{{ℒ}_1}$ is the reduct to ${ℒ}_1$, and $f:{𝒜}_1\to {ℬ}_1$ is an embedding of ${𝒜}_1$ into another ${ℬ}_1\in {𝕂}_1$, there is an expansion of ${ℬ}_1$ to an ${ℒ}_2$-structure ${ℬ}_2\in {𝕂}_2$ such that $f$ is an embedding ${𝒜}_2\to {ℬ}_2$. The Fraïssé limit of ${𝕂}_1$ is the reduct to ${ℒ}_1$ of the Fraïssé limit of ${𝕂}_2$ if and only if $({𝕂}_1,{𝕂}_2)$ is reasonable.

Recall that

Note that ${ℒ}_0=\{U_{\mathrm{\varnothing }}\}$. Let $T_k=T_{\pi }\mathrm{\upharpoonright }{ℒ}_k$ be the restriction of $T_{\pi }$ to the axioms of $T_{\pi }$ with symbols from ${ℒ}_k$, namely with the following axioms from $T_{\pi }$:

1. for each $\sigma \nprec \pi$ and $\sigma \in {\{0,1,2,\mathrm{\dots },k-1\}}^{\le k}$,

   $$\neg \exists x{U}_{\sigma }(x),$$

2. for each $\sigma \prec \pi$, $\sigma \in {\{0,1,2,\mathrm{\dots },k-1\}}^{\le k}$, with $\mathrm{\ell }$ such that $\sigma \mathrm{\ell }\prec \pi$, and ,

   $$U_{\sigma }(x)⟶\forall \overline{y}[P_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)].$$

Any axiom of $T_{\pi }$ which does not appear as an axiom of $T_k$ includes some symbol from $ℒ-{ℒ}_k$. (We do not worry at this point about whether $T_{\pi }$ has some consequences in ${ℒ}_k$ which are proven by axioms not in ${ℒ}_k$. This will be resolved by Claim 3.)

We will recursively define universal ${ℒ}_k$-theories $T_k^{\ast }$ for $k\in \mathbb{N}$. For each $k$, $𝕂(T_k^{\ast })$ will be a Fraïssé class with $(𝕂(T_k^{\ast }),𝕂(T_{k+1}^{\ast }))$ being reasonable. Let $S_k\supseteq T_k^{\ast }$ be the ${ℒ}_k$-theory of the Fraïssé limit of $𝕂(T_k^{\ast })$. This is a complete, consistent extension of $T_k^{\ast }$ which is $\omega$-categorical and admits quantifier elimination. Since the Fraïssé limit of $𝕂(T_k^{\ast })$ is a reduct to ${ℒ}_k$ of the Fraïssé limit of $𝕂(T_{k+1}^{\ast })$, we will have that $S_k=S_{k+1}{\mathrm{\upharpoonright }}_{{ℒ}_k}$.

We will begin with $T_0^{\ast }=T_0$ and will ensure that $T_{k+1}^{\ast }\cup S_k\vDash T_{k+1}$. Since $S_{k+1}\vDash T_{k+1}^{\ast }$, as it is the theory of the Fraïssé limit of $T_{k+1}^{\ast }$, and because $S_{k+1}\vDash S_k$ by reasonableness, we will have $S_{k+1}\vDash T_{k+1}$. Letting $S={\bigcup }_{k\in \omega }{S}_k$, and after verifying that $S\vDash \exists x{U}_{\sigma }(x)$ for every $\sigma \prec \pi$, we will get a complete $ℒ$-theory with $S\vDash T_{\pi }\cup \{\exists x{U}_{\sigma }(x):\sigma \prec \pi \}$ and hence $S\vDash T$.

Beginning with $T_0^{\ast }=T_0$, this has no axioms as ${ℒ}_0$ has only the symbol $U_{\mathrm{\varnothing }}$. This is of course a Fraïssé class and has as its Fraïssé limit infinitely many elements satisfying, and infinitely many elements not satisfying, $U_{\mathrm{\varnothing }}$. Now given the ${ℒ}_{k-1}$-theory $S_{k-1}$ we will define $T_k^{\ast }$. Since $S_{k-1}$ admits quantifier elimination, there is a quantifier-free ${ℒ}_{k-1}$-formula $Q_{k-1}(\overline{y})$ such that $S_{k-1}\vDash P_{k-1}(\overline{y})⟷Q_{k-1}(\overline{y})$. We will have already defined, for each , an ${ℒ}_i$-formula $Q_i(\overline{y})$ such that $S_i\vDash P_i(\overline{y})⟷Q_i(\overline{y})$. Since $S_{k-1}\vDash S_i$, this equivalence is also true modulo $S_{k-1}$. We are now ready to define $T_k^{\ast }$, which has the following axioms:

1. for each $\sigma \nprec \pi$, $\sigma \in {\{0,1,2,\mathrm{\dots },k-1\}}^{\le k}$,

   $$\neg \exists x{U}_{\sigma }(x)$$

2. for each $\sigma \prec \pi$, $\sigma \in {\{0,1,2,\mathrm{\dots },k-1\}}^{\le k}$, with $\mathrm{\ell }$ such that $\sigma \mathrm{\ell }\prec \pi$, and

   $$U_{\sigma }(x)⟶\forall \overline{y}[Q_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)].$$

($1^{\ast }$) is exactly the same as ($1^{\prime }$), and ($2^{\ast }$) is the same as ($2^{\prime }$) except with $Q_i(\overline{y})$ replacing $P_i(\overline{y})$. So $T_k^{\ast }$ includes, for each axiom of $T_k$, an axiom which is equivalent modulo $S_{k-1}$. Thus $T_k^{\ast }\cup S_{k-1}\vDash T_k$ and $T_k\cup S_{k-1}\vDash T_k^{\ast }$. We also have that $T_k^{\ast }\vDash T_{k-1}^{\ast }$ as each axiom of $T_{k-1}^{\ast }$ is an axiom of $T_k^{\ast }$.

The point of defining $T_k^{\ast }$ is that it is a universal theory and hence $𝕂(T_k^{\ast })$ has the HP. The next two lemmas complete the verification that $𝕂(T_k^{\ast })$ is a Fraïssé class.

Claim 1.

$𝕂(T_k^{\ast })$ has the JEP.

Proof.

Let $𝒜,ℬ\vDash T_k^{\ast }$. We define a sort of free amalgam $𝒞$ of $𝒜$ and $ℬ$. The domain of $𝒞$ is the disjoint union $C=A\bigsqcup B$ of the domains of $𝒜$ and $ℬ$. For any tuple contained entirely in $𝒜$ or $ℬ$, let $𝒞$ inherit the relations from $𝒜$ and $ℬ$. Since the $U_{\sigma }$ and $A_i$ are unary relations, this defines them completely on $𝒞$. It remains to define the relations $V_{i,\sigma }$ for tuples $(\overline{y},x)$ that are not fully contained in $𝒜$ or $ℬ$. On these tuples we would like to set these relations so that $𝒞\vDash V_{i,\sigma }(\overline{y},x)⟷Q_i(\overline{y})$, but we must do this recursively so that when we are defining $V_{i,\sigma }$ we have already determined $Q_i(\overline{y})$. First, for $V_{0,\sigma }\in {ℒ}_k$ and $(\overline{y},x)$ not fully contained in $𝒜$ or $ℬ$, set $𝒞\vDash V_{0,\sigma }(\overline{y},x)$ if and only if $𝒞\vDash Q_0(\overline{y})$. $Q_0$ is an ${ℒ}_0$-formula, and the reduct of $𝒞$ to ${ℒ}_0=\{U_{\mathrm{\varnothing }}\}$ is already defined. Once all $V_{i,\sigma }\in {ℒ}_k$ for have been determined, we can set $𝒞\vDash V_{n,\sigma }(\overline{y},x)$ if and only if $𝒞\vDash Q_n(\overline{y})$ which is well-defined as $Q_n$ is an ${ℒ}_n$-formula and the reduct of $𝒞$ to ${ℒ}_n$ has already been defined. We can see that for all $(\overline{y},x)$ not fully included in $𝒜$ or $ℬ$ we have $𝒞\vDash Q_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)$.

We must now check that $𝒞\vDash T_k^{\ast }$. The axioms ($1^{\ast }$) are immediate, since the $U_{\sigma }$ are unary and each element of $𝒞$ is in either $𝒜$ or $ℬ$ both of which satisfy ($1^{\ast }$). For ($2^{\ast }$), suppose that $𝒞\vDash U_{\sigma }(x)$ and $x\in 𝒜$. For $\overline{y}\in 𝒜$, since $𝒜\vDash T_k^{\ast }$ we have $𝒞\vDash Q_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)$, and for tuples $\overline{y}$ not completely contained in $𝒜$ by construction we have $𝒞\vDash Q_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)$. The case where $x\in ℬ$ is identical. So we have verified that $𝒞\vDash T_k^{\ast }$. ∎

Claim 2.

$𝕂(T_k^{\ast })$ has the AP.

Proof.

Given $𝒜,ℬ,𝒞\vDash T_k^{\ast }$ with $𝒜\subseteq ℬ$ and $𝒜\subseteq 𝒞$, we must form the amalgam $𝒟$ of $ℬ$ and $𝒞$ over $𝒜$. This will be a free amalgam of $ℬ$ and $𝒞$ with domain $D=B\cup C$. It is clear this free amalgam makes the diagram commute, so all that is left to do is assign relations.

As for the JEP, let $𝒟$ inherit the relations from $ℬ,𝒞$ for tuples solely contained in $ℬ,𝒞$. For tuples entirely contained in their intersection $𝒜$, we know that $ℬ,𝒞$ agree on the relations. It only remains to assign tuples that are not entirely contained in either $ℬ$ or $𝒞$. As before, we inductively assign $V_{i,\sigma }$ on such tuples $(\overline{y},x)$ so that $𝒟\vDash Q_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)$. The argument that $𝒟\vDash T_k^{\ast }$ is again the same as for the JEP, with ($1^{\ast }$) being relatively immediate and ($2^{\ast }$) following from the fact that for new tuples $(\overline{y},x)$ we have $𝒟\vDash Q_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)$. ∎

Since $T_k^{\ast }\vDash T_{k-1}^{\ast }$, for any $𝒜\in 𝕂(T_k^{\ast })$ the reduct of $𝒜$ to ${ℒ}_{k-1}$ is in $𝕂(T_{k-1}^{\ast })$. So $𝕂(T_k^{\ast })$ is an expansion class of $𝕂(T_{k-1}^{\ast })$. We now verify that it is reasonable.

Claim 3.

$(𝕂(T_{k-1}^{\ast }),𝕂(T_k^{\ast }))$ is reasonable.

Proof.

Let $𝒜,ℬ\vDash T_{k-1}^{\ast }$ be such that $𝒜\subseteq ℬ$. Let ${𝒜}^{\ast }\vDash T_k^{\ast }$ be an expansion of $𝒜$ to an ${ℒ}_k$-structure. We must construct ${ℬ}^{\ast }\vDash T_k^{\ast }$ an expansion of $ℬ$ such that ${𝒜}^{\ast }\subseteq {ℬ}^{\ast }$. Note that

${ℒ}_k-{ℒ}_{k-1}=\{U_{\sigma }$ $:\sigma \in 𝔗\cap {\{0,1,\mathrm{\dots },k-1\}}^{\le k}\setminus {\{0,1,\mathrm{\dots },k-2\}}^{\le k-1}\}\cup \{A_{k-1}\}$

$\cup \{V_{k-1,\sigma }:\sigma \in 𝔗\cap {\{0,1,\mathrm{\dots },k-1\}}^{\le k}\}.$

To define the relations on ${ℬ}^{\ast }$, let all relations from ${𝒜}^{\ast }$ carry over. For tuples not fully contained in ${𝒜}^{\ast }$, let $A_{k-1}$ be false and all new $U_{\sigma }$ be false. It remains to set the $V_{i,\sigma }$ that are introduced in ${ℒ}_k$ for tuples that are not exclusively in ${𝒜}^{\ast }$. Since the quantifier-free formulas $Q_i$, , only use symbols from ${ℒ}_i\subseteq {ℒ}_{k-1}$, it is already determined whether $ℬ\vDash Q_i(\overline{y})$. For tuples $(\overline{y},x)$ not entirely contained in ${𝒜}^{\ast }$ we can simply set ${ℬ}^{\ast }\vDash V_{i,\sigma }(\overline{y},x)$ if and only if $ℬ\vDash Q_i(\overline{y})$.

It remains to verify that ${ℬ}^{\ast }\vDash T_k^{\ast }$. We already know that $ℬ\vDash T_{k-1}^{\ast }$, so we just need to check the new axioms. New axioms of the form ($1^{\ast }$) are all of the form $\neg \exists x{U}_{\sigma }(x)$ with $U_{\sigma }\in {ℒ}_k-{ℒ}_{k-1}$. For $x\in {𝒜}^{\ast }$ we have $\neg U_{\sigma }(x)$ as ${𝒜}^{\ast }\vDash T_k^{\ast }$, and for $x\notin {𝒜}^{\ast }$ recall that we set $\neg U_{\sigma }(x)$.

Now we consider axioms of the form ($2^{\ast }$). Such an axiom is of the form

$$U_{\sigma }(x)⟶\forall \overline{y}[Q_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)]$$

where $\sigma \prec \pi$, $\mathrm{\ell }$ is such that $\sigma \mathrm{\ell }\prec \pi$, and . It is equivalent to check that for each $x\in {ℬ}^{\ast }$ and that

$${ℬ}^{\ast }\vDash U_{\sigma }(x)⟶\forall \overline{y}[Q_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)]$$

For such an axiom to be new, one of $U_{\sigma }$ or $V_{i,\sigma }$ are in ${ℒ}_k-{ℒ}_{k-1}$. If $U_{\sigma }\in {ℒ}_k-{ℒ}_{k-1}$, then $\sigma \in 𝔗\cap {\{0,1,\mathrm{\dots },k-1\}}^{\le k}-{\{0,1,\mathrm{\dots },k-2\}}^{\le k-1}$, so $V_{i,\sigma }\notin {ℒ}_{k-1}$. Thus for any such new axiom we have $V_{i,\sigma }\in {ℒ}_k-{ℒ}_{k-1}$ is a new symbol. Suppose $x\in {𝒜}^{\ast }$ and $U_{\sigma }(x)$. Then for $\overline{y}$ entirely contained in ${𝒜}^{\ast }$ we have ${𝒜}^{\ast }\vDash Q_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)$ since ${𝒜}^{\ast }\vDash T_k^{\ast }$. For $\overline{y}$ not completely contained in ${𝒜}^{\ast }$, by construction we have that ${ℬ}^{\ast }\vDash Q_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)$. Thus ${ℬ}^{\ast }\vDash \forall \overline{y}[Q_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)]$. If $x\notin {𝒜}^{\ast }$, then whether or not we have ${ℬ}^{\ast }\vDash U_{\sigma }(x)$, by construction ${ℬ}^{\ast }\vDash \forall \overline{y}[Q_i(\overline{y})⟷V_{i,\sigma }(\overline{y},x)]$. Thus ${ℬ}^{\ast }\vDash T_k^{\ast }$, so $(𝕂(T_{k-1}^{\ast }),𝕂(T_k^{\ast }))$ is reasonable. ∎

Let $S_k$ be the complete theory of the Fraïssé limit of $𝕂(T_k^{\ast })$, which is $\omega$-categorical and admits quantifier elimination. Since $(𝕂(T_{k-1}^{\ast }),𝕂(T_k^{\ast }))$ is reasonable, $S_k{\mathrm{\upharpoonright }}_{{ℒ}_{k-1}}=S_{k-1}$. Let $S={\bigcup }_k{S}_k$. This is a complete $ℒ$-theory. Since each $S_k$ admits quantifier elimination, so does $S$.

Claim 4.

For each $\sigma \prec \pi$, $S\vDash \exists x{U}_{\sigma }(x)$.

Proof.

Fix $\sigma \prec \pi$. It suffices to show that for some $k$, $S_k\vDash \exists x{U}_{\sigma }(x)$. Since $S_k$ is the Fraïssé limit of $T_k^{\ast }$, it suffices to show that there is a model of $𝒜\vDash T_k^{\ast }$ with $𝒜\vDash \exists x{U}_{\sigma }(x)$. Let $k$ be large enough that $U_{\sigma }\in {ℒ}_k$. We can take $𝒜$ to have a single element $a$ satisfying $U_{\sigma }$ and no other $U_{\tau }\in {ℒ}_k$. This element $a$ will also satisfy no $A_i\in {ℒ}_k$, and we can inductively define the $V_{i,\tau }\in {ℒ}_k$ such that $𝒜\vDash Q_i(a,\mathrm{\dots },a)⟷V_{i,\tau }(a,\mathrm{\dots },a,a)$. Thus, checking axioms of types ($1^{\ast }$) and ($2^{\ast }$), we see that $𝒜\vDash T_k$. ∎

For each $k$, $S\vDash T_k^{\ast }\cup S_{k-1}\vDash T_k$ and so $S\vDash T_{\pi }$. Hence $S$ is a completion of $T_{\pi }\cup \{\exists x{U}_{\sigma }(x):\sigma \prec \pi \}$ and hence, as discussed earlier, $S$ is a completion of $T$.

Now let $S^{+}$ be the Marker extension of $S$ where we make each $A_i$ and $U_{\sigma }$ universal. Since $S$ is consistent, so is $S^{+}$ (Lemma 3.1). Also $S$ has property ($\ast$) as each $\sigma$ of length $1$ is in $𝔗$ (as $\mathrm{\varnothing }$ has a child in $𝔗$ and hence all of its possible children are in $𝔗$) but $S\vDash \forall x\neg U_{\sigma }(x)$ for all $\sigma \nprec \pi$. Recall that it is the $\neg U_{\sigma }$ that are made existential in the Marker extension. $S^{+}$ is complete and by Lemma 3.6 it is a completion of $T^{+}$. We will now argue that $S^{+}$ is not relatively decidable.

Claim 5.

$S^{+}$ is not relatively decidable.

Proof.

It suffices to show that for each formula $\phi (\overline{x})$ such that $S^{+}\vDash \exists \overline{x}\phi (\overline{x})$, the ${ℒ}^{+}\cup \{\overline{c}\}$-theory $S^{+}\cup \{\phi (\overline{c})\}$ is not model complete. Fix some such formula $\phi (\overline{x})$. Let $k$ be such that $\phi (\overline{x})$ is an ${ℒ}_k^{+}$-formula. By Lemma 3.2, $\phi (\overline{x})$ is equivalent to a quantifier-free formula in the language ${ℒ}_k^{+}\cup \{{\psi }^{\ast }:\psi \text{ an }{ℒ}_k\text{-formula}\}$. Since $S_k$ admits quantifier elimination, $\phi (\overline{x})$ is in fact equivalent to a quantifier-free formula in the language ${ℒ}_k^{+}\cup \{{\psi }^{\ast }:\psi \text{ a quantifier-free }{ℒ}_k\text{-formula}\}$. Choose $j>k$ sufficiently large so that for any $\sigma \prec \pi$ with $U_{\sigma }\in {ℒ}_k$, $j$ is greater than any entry of $\sigma$ and also greater than the next entry of $\pi$ following all such $\sigma$.

We will show that $S^{+}\cup \{\phi (\overline{c})\}$ is not model complete by showing that $A_j$ is not equivalent to an existential formula. Given ${𝒜}^{+}\vDash S^{+}$ and $\overline{c}\in {𝒜}^{+}$ such that ${𝒜}^{+}\vDash \phi (\overline{c})$ and with some $d\in {𝒜}^{+}$ such that ${𝒜}^{+}\vDash A_j(d)$, we will construct a model ${𝒞}^{+}\supseteq {𝒜}^{+}$ with ${𝒞}^{+}\vDash S^{+}\cup \{\phi (\overline{c})\}$ and such that ${𝒞}^{+}\vDash \neg A_j(d)$.

We will now argue that we may assume that $\overline{c}$ is entirely contained within the first sort of ${𝒜}^{+}$. If not, we may also split $\overline{c}$ into a pair of tuples ${\overline{c}}_1$ in the first sort $S_1$ and ${\overline{c}}_2$ in the second sort $S_2$, so that $\phi$ can be written as $\phi ({\overline{x}}_1,{\overline{x}}_2)$. Consider all of the atomic and negated atomic terms, in the language ${ℒ}_k^{+}\cup \{{\psi }^{\ast }:\psi \text{ a quantifier-free }{ℒ}_k\text{-formula}\}$, which appear in $\phi ({\overline{x}}_1,{\overline{x}}_2)$. Since ${𝒜}^{+}\subseteq {𝒞}^{+}$, the truth value of any atomic or negated atomic formula from ${ℒ}_k^{+}$ is maintained from ${𝒜}^{+}$ to ${𝒞}^{+}$. It is only the formulas ${\psi }^{\ast }$ which may change their truth value. Any such formula can only be true of elements in the first sort, and so if applied to a tuple including any element of ${\overline{c}}_2$ must be false in both ${𝒜}^{+}$ and ${𝒞}^{+}$. Thus, essentially, we only need to be concerned with ${\overline{c}}_1$, as ${\overline{c}}_2$ poses no obstacle.

Let $𝒜$ be the model of $S$ associated with ${𝒜}^{+}$. Let $ℬ$ be the same as $𝒜$ except that $ℬ\vDash \neg U_{\sigma }(x)$ for all $x$ of the appropriate sort where $U_{\sigma }\notin {ℒ}_k$, and also $ℬ\vDash \neg A_j(d)$. Then $𝒜$ is a weak substructure of $ℬ$, $𝒜{\subseteq }_wℬ$. If ${ℬ}^{+}$ is the Marker extension of $ℬ$, then by Lemma 3.5, ${𝒜}^{+}\subseteq {ℬ}^{+}$. Since $j>k$ the reducts of $𝒜$ and $ℬ$ to ${ℒ}_k$ are the same, and as $\phi$ is an ${ℒ}_k^{+}$-formula, we have ${ℬ}^{+}\vDash \phi (\overline{c})$. Now we argue that $ℬ$ satisfies the universal part of $S$.

Subclaim.

$ℬ\vDash S_{\forall }$.

Proof.

Since $S={\bigcup }_m{S}_m$, any universal consequence of $S$ is also a consequence of one of the ${ℒ}_m$-theories $S_m$. The theories $S_m$ are the Fraïssé theories of the Fraïssé classes $𝕂(T_m^{\ast })$, and so it suffices to show that $ℬ\vDash T_m^{\ast }$ for every $m$.

Using the fact that the reduct of $𝒜$ to ${ℒ}_m$ is a model of $T_m^{\ast }$, we argue that $ℬ$ is also a model of $T_m^{\ast }$. We satisfy the axioms of type $(1^{\ast })$ trivially since none of the elements of $𝒜$ satisfied $U_{\sigma }(x)$ for $\sigma \nprec \pi$, and in $ℬ$ we did not add any new elements or change any relations from $\neg U_{\sigma }$ to $U_{\sigma }$. Recalling the form of axioms of type $(2^{\ast })$, for each $\sigma \prec \pi$ and $\mathrm{\ell }$ such that $\sigma \mathrm{\ell }\prec \pi$, and , we will verify that

$$ℬ\vDash \forall x[U_{\sigma }(x)⟶\forall \overline{y}[Q_i(\overline{y})\leftrightarrow V_{i,\sigma }(\overline{y},x)]].$$

Note that these are more axioms than appear in $T_m^{\ast }$, as we are only assuming that and not , but as these axioms are all true anyway there is no reason to assume . We will only consider those $U_{\sigma }\in {ℒ}_k$, since all other $U_{\sigma }$ were set to false in $ℬ$. Such $\sigma$ are of length at most $k$ and satisfy $\sigma \in {\{0,1,\mathrm{\dots },k-1\}}^{\le k}$, so $\sigma \mathrm{\ell }$ is at most length $k+1$. We do not have a bound on $\mathrm{\ell }$, though we do know that $j>\mathrm{\ell }$.

Fix $\sigma$ and $x\in ℬ$ and assume $ℬ\vDash U_{\sigma }(x)$. Consider some $Q_i(\overline{y})$ for . It is a quantifier-free formula in ${ℒ}_i$. Our goal is to make sure that $ℬ\vDash Q_i(\overline{y})\leftrightarrow V_{i,\sigma }(\overline{y},x)$ for each . Since we did not change the truth value of $V_{i,\sigma }$, it suffices to show that we did not change the truth value of $Q_i(\overline{y})$. Since $Q_i$ is quantifier-free in ${ℒ}_i$, it suffices to show that we did not change the truth value of any atomic formula that $Q_i$ is composed of. If $\mathrm{\ell }\le k$, then we know $Q_i$’s truth value is preserved since the reducts of $𝒜$ and $ℬ$ to ${ℒ}_k$ are equal. Thus assume $\mathrm{\ell }\ge k+1$. First note that all $A_i$ for remain the same as in $𝒜$ (we only changed $A_j$, with $j>\mathrm{\ell }$) as do all $V_{i,\sigma }$ for any $i,\sigma$. Thus by ensuring that any $U_{\tau }$ in $Q_i$ has the same truth value as it does in $𝒜$, we know that $Q_i$ will have the same truth value as $V_{i,\sigma }$. We only consider $\tau \prec \pi$ since all others are false in both $𝒜$ and $ℬ$. We claim that if $U_{\tau }$ appears in $Q_i$ for then $U_{\tau }\in {ℒ}_k$. For the sake of contradiction, assume that $U_{\tau }\in ℒ-{ℒ}_k$. Thus $\tau \in 𝔗\setminus {\{0,1,\mathrm{\dots },k-1\}}^{\le k}$. Either $\tau$ has length at least $k+1$ or there is $n\ge k$ such that $n$ appears as an entry in $\tau$. In the second case, note that $\sigma$ does not have $n$ as an entry and so $\sigma \prec \tau$.

Case 1.

$\tau$ has length $\ge k+1$. Since $\tau \prec \pi$ and is of length $\ge k+1$, we know $\tau$ must be $\sigma \mathrm{\ell }$ or an extension of it. However, recall that $U_{\tau }\in {ℒ}_i\subseteq {ℒ}_{\mathrm{\ell }-1}$, which only contains $U_{\rho }$ for $\rho \in {\{0,1,\mathrm{\dots },\mathrm{\ell }-2\}}^{\le \mathrm{\ell }-1}$, so $\tau$ cannot possibly contain $\mathrm{\ell }$. This yields a contradiction.

Case 2.

There is $n\ge k$ such that $n$ appears in $\tau$. Recall that $\mathrm{\ell }\ge k+1$. Since $\sigma \in {\{0,1,\mathrm{\dots },k-1\}}^{\le k}$, $\sigma$ cannot contain $n$ as any entry, and so $\tau$ cannot be an initial segment of $\sigma$. Since $\sigma$ and $\tau$ are compatible, we have $\sigma \prec \tau \prec \pi$. Thus $\sigma \mathrm{\ell }⪯\tau$. Since $U_{\tau }$ is contained in $Q_i$, a quantifier-free formula in ${ℒ}_i$, it must be that $\tau \in {\{0,1,\mathrm{\dots },\mathrm{\ell }-2\}}^{\le \mathrm{\ell }-1}$, since . This yields a contradiction.

Thus we have shown that $U_{\tau }\in {ℒ}_k$. We conclude that $Q_i$ has the same truth value in $ℬ$ as in $𝒜$ and so axioms of the form $(2^{\ast })$ are fulfilled. Since $ℬ\vDash T_m^{\ast }$ for each $m$, $ℬ\vDash S_{\forall }$, completing the proof of the subclaim. ∎

Since $ℬ\vDash S_{\forall }$, standard model-theoretic results imply that there is $𝒞\supseteq ℬ$ with $𝒞\vDash S$. Let ${𝒞}^{+}$ be the Marker extension of $𝒞$, so that ${𝒞}^{+}\vDash S^{+}$, with ${𝒜}^{+}\subseteq {ℬ}^{+}\subseteq {𝒞}^{+}$. We have ${𝒞}^{+}\vDash \neg A_j(d)$. It remains to argue that ${𝒞}^{+}\vDash \phi (\overline{c})$. Recall that in models of $S^{+}$, $\phi$ is equivalent to a quantifier-free formula in the language ${ℒ}_k^{+}\cup \{{\psi }^{\ast }:\psi \text{ a quantifier-free }{ℒ}_k\text{-formula}\}$. So it suffices to show that ${𝒜}^{+}$ is a substructure of ${𝒞}^{+}$ in this language, as then since ${𝒜}^{+}\vDash \phi (\overline{c})$, we can conclude that ${𝒞}^{+}\vDash \phi (\overline{c})$. Since ${𝒜}^{+}$ is an ${ℒ}^{+}$-substructure of ${𝒞}^{+}$, it remains to check that if a relation ${\psi }^{\ast }$ holds of some tuple in ${𝒜}^{+}$ then it holds in ${𝒞}^{+}$ for $\psi$ a quantifier-free ${ℒ}_k$-formula. This follows from the fact that, after taking their reducts to ${ℒ}_k$, $𝒜$ is a substructure of $ℬ$ and $ℬ$ is a substructure of $𝒞$. This completes the argument of the claim. ∎

This completes the proof of the theorem: If $𝔗$ is well-founded, then the theory $T^{+}$ constructed is relatively decidable, and if $𝔗$ is ill-founded then the theory $S^{+}\supseteq T^{+}$ is not relatively decidable and hence $T^{+}$ is not relatively decidable. ∎