Complexity of the computable entailment relation

Question

The following definition comes from Richard Shore's 2010 paper 'Reverse Mathematics: The Playground of Logic'.

Let $\varphi$ and $\psi$ be sentences in the language of second order arithmetic $\mathrm{L}_2$. $\psi$ computably entails $\varphi$, $\psi \models_\mathcal{C} \varphi$, just in case for every Turing ideal $\mathcal{C}$ the $\omega$-model with $\mathcal{C}$ as its second-order part which satisfies $\psi$ also satisfies $\varphi$.

I'm interested in the recursion-theoretic complexity of the computable entailment relation. Which sets $A \subseteq \omega$ are recursive or recursively enumerable by a Turing machine with an oracle for this relation? Can it be shown that it's equivalent to some well-studied recursion-theoretic principle?

Answer 1

The answer is that the relation $C(\phi)$ defined as "every Turing ideal satisfies $\phi$" is $\Pi^1_1$ complete.

To obtain a lower bound, it's enough to show that a $\Pi^1_1$ sentence of second-order arithmetic is true if and only if it is true in every Turing ideal. Half of this equivalence follows from the fact that the standard model is a Turing ideal, so anything false is false in that ideal. Conversely, any Turing ideal in which a $\Pi^1_1$ statement is false yields a counterexample to the statement which is still a counterexample in the standard model. The key point is that any arithmetical property of a real is absolute to all Turing ideals, including the standard model. Thus the satisfaction relation for $\Pi^1_1$ formulas agrees with the $C$ relation, and so the latter is $1$-reducible to the former.

To get the matching upper bound we have to show that $C(\phi)$ can be defined by a $\Pi^1_1$ formula. To do this, we need a little lemma.

Lemma. If a sentence of second-order arithmetic is false in any Turing ideal then it is false in a countable Turing ideal.

To prove this, suppose $\phi$ is false in an ideal $I$. View $I$ as an $\omega$-model in the language of second-order arithmetic. By the downward Lowenheim-Skolem theorem, there is a countable elementary substructure $S$ of $I$. Then $S$ will be an $\omega$-model because it is a substructure of an $\omega$-model, and $S$ will be a Turing ideal, because this property of an $\omega$-model is definable by a formula of second-order arithmetic that was true in $I$. And $\phi$ will be false in $S$, again because it was false in $I$.

Thus, in light of the lemma, a sentence of second-order arithmetic is true in every Turing ideal if and only if it is true in every countable Turing ideal.

Now consider the formula $C'(\phi)$ which says "every countable Turing ideal satisfies $\phi$". The relation $C'$ can be expressed in second-order arithmetic as "For every $X$, for every $Y$, if $X$ codes a Turing ideal and $Y$ is the satisfaction predicate for $X$ then $Y(\phi) = 1$". Here "$X$ codes a Turing ideal" means that the class $\{ \{ m: 2^n3^m \in X\} : n \in \omega\}$ is a Turing ideal. . The two hypotheses of the if statement in the definition are both expressible by arithmetical formulas with parameters for $X$ and $Y$, so the entire formula is $\Pi^1_1$.

Hence the $C$ relation is $1$-reducible to the satisfaction relation for $\Pi^1_1$ sentences. Thus, by Myhill's theorem, $C$ is $1$-equivalent to that satisfaction relation.

Answer 2

I don't have a full answer to your question, but I can throw out some thoughts:

First, note that second order arithmetic and its subsystems are still in first order logic. So models and all the logical rules are still the same.

It suffices to instead of considering $\psi \models_C \varphi$ to consider $\models_C \psi \Rightarrow \varphi$. So an interesting related to question to consider what formulas $\varphi$ such that $\models_C \varphi$.

By definition $\models_C \varphi$ holds if $\varphi$ holds in all $L_2$ structures whose first order part is $\omega$ and whose second order parts (the collection of subsets of the first order part) is a Turing Ideal. $\omega$ models whose second order parts are Turing Ideal are exactly the $\omega$-models of $\text{RCA}_0$. Hence all results provable in $\text{RCA}_0$ is "computably entailed"

Now you can look at particular $\omega$-models. $REC$ is the minimal $\omega$-model consisting of just the computable sets. Hence all computably entailed formulas are a subset of the full theory of $\text{REC}$. Since it is minimal, all $\Sigma_1^1$ formulas true in $\text{REC}$ are exactly the computably entailed formulas. However, the full theory of $\text{REC}$ is probably not all the computably entailed formulas since you can formalize computability within second order arithmetics. You can then write the $\Pi_1^1$ formula stating that every set is computable, i.e. $(\forall X)(\exists e)(\forall z)(z \in X \Rightarrow \Phi_e(z) = 1 \wedge z \notin X \Rightarrow \Phi_e(z) = 0)$. $\text{REC}$ would model this sentence, but any other $\omega$ model would not.

Answer 3

Here is what seems to me like a cheap way of obtaining a lower bound.

---

Let $\mathrm{L}_1$ denote the language of first order arithmetic, i.e. $\mathrm{L}_2$ with set variables omitted, and fix a Gödel coding. Now let

$$A = \left\{ \ulcorner \varphi \urcorner : \; \models_\mathcal{C} \varphi \wedge \varphi \in \mathrm{L}_1 \right\}.$$

Since the $\mathrm{L}_1$-formulae $\varphi$ true in an $\omega$-model are precisely those such that $\mathbb{N} \models \varphi$, it looks like $A = Th(\mathbb{N})$. And since $A$ is recursive in $\models_\mathcal{C}$ we get that $Th(\mathbb{N}) \leq_T \; \models_\mathcal{C}$.

By a standard result, $0^{(\omega)} \equiv_T Th(\mathbb{N})$, so $0^{(\omega)} \leq_T \; \models_\mathcal{C}$.