# Complexity of the computable entailment relation

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?

-

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.

-
Thanks so much Carl, this is perfect. I spent some time going through your proof and am pretty happy I grasp most of the steps. Could you say a little more about the absoluteness of the arithmetical properties of reals to all Turing ideals? –  Benedict Eastaugh Oct 1 '12 at 13:40
@Benedict: This is a reflection of the fact that in second-order arithmetic any arithmetical formula with set parameters has the same truth value in every $\omega$-model that contains the parameters. Comparing definitions, "truth in a Turing ideal" is defined the same as "truth in an $\omega$ model". The absoluteness is because the quantifiers can only range over $\omega$, which is the same in every $\omega$-model, and all the symbols in the signature have the same interpretation. A formal proof would be by structural induction on the class of arithmetical formulas with those set parameters. –  Carl Mummert Oct 1 '12 at 19:38

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.

-
Thanks, this is a helpful start. Could you explain a bit more why REC being the minimal $\omega$-model means that all $\Sigma^1_1$ formulae true in it are exactly the computably entailed ones? (I presume that here you mean the $\Sigma^1_1$ computably entailed ones.) It seems like it should be obvious, but right now I can't quite see it. –  Benedict Eastaugh Jul 4 '12 at 1:01
REC is the $\omega$-model consisting of just the computable sets. You can prove (see Simpson Subsystem of Second Order Arithemetic) that all $\omega$-models of $RCA_0$ are Turing Ideals. Intuitively, $RCA_0$ asserts the existence of all $\Delta_1^0$ definable sets with parameters. In $\omega$, these are just the computable sets (relative to sets that exists). Hence the smallest one and also the smallest Turing Ideal in $\omega$ is $REC$. –  William Jul 4 '12 at 5:01
$\Sigma_1^1$ sentences $\psi$ take the form $(\exists X)\varphi$ where $\varphi$ is an arithmetical formula. $REC$ is an $\omega$ models of with second order part a Turing Ideal, so if $\psi$ is computably entailed, then you must have $REC \models \psi$. Now suppose $REC \models \psi$, i.e. $REC \models (\exists X)\varphi$. Since the second order part is $REC$ is the subset of the second order part of every other $\omega$-model that is a Turing Ideal, the $(\exists X)$ witness still holds. Thus every such model also models $\psi$. So the $\Sigma_1^1$ formula are exactly characterized. –  William Jul 4 '12 at 5:04
Ah, ok, so this is just about the (upwards) absoluteness of existential quantification (since all $\omega$-models whose second order parts are Turing ideals extend REC). Thanks. –  Benedict Eastaugh Jul 4 '12 at 5:32
It's worth mentioning that we can strengthen one of your points. If $\mathsf{RCA} \vdash \varphi$ then $\models_\mathcal{C} \varphi$, since all $\omega$-models satisfy the full second order induction scheme. There are some details on a previous question of mine. –  Benedict Eastaugh Jul 11 '12 at 4:30

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}$.

-
Along the same lines, suppose $<_e$ is a computable linear order. Then $<_e$ is a well ordering if and only if every Turing ideal $\mathcal{C}$ models "$<_e$ is a well ordering" - for if there is an infinite descending sequence $f$ then the ideal generated by $f$ is a counterexample, and vice versa. Thus $\vDash_\mathcal{C}$ computes at least the $\Pi^1_1$ theory of the standard model of arithmetic, which is a slight extension of your result. –  Carl Mummert Sep 26 '12 at 12:03
My hasty conjecture is that $\models_\mathcal{C}$ is equivalent to the $\Pi^1_1$ theory. It would be enough to show that if a sentence is false in any Turing ideal then it is false in some countably generated (i.e. countable) Turing ideal. This is because the statement "$\phi$ is true in every countably generated Turing ideal" should itself be $\Pi^1_1$ for every $\phi \in L_2$. The idea there is that a countably generated Turing ideal is essentially a countable coded $\omega$ model, and for each $\phi \in L_2$ the statement "$\phi$ holds in every countable coded $\omega$ model" is $\Pi^1_1$. –  Carl Mummert Sep 26 '12 at 12:11