<p>The answer is <strong>yes</strong>.</p>
<p>This was proved by Hanf (<a href="https://www.sciencedirect.com/science/article/abs/pii/B9780720422337500204" rel="nofollow noreferrer"><em>Model-theoretic methods in the study of elementary logic</em>, in the <strong>Theory of models</strong> volume</a>). A &quot;uniform&quot; version of this result was conjectured by Hanf and proved by Peretyat'kin in his book <a href="https://rads.stackoverflow.com/amzn/click/com/0306110628" rel="nofollow noreferrer" rel="nofollow noreferrer"><em>Finitely axiomatizable theories</em></a>; I don't have access to that book, but <a href="https://arxiv.org/pdf/2212.03565.pdf" rel="nofollow noreferrer">Visser's <em>Essential hereditary undecidability</em></a> cites it as Theorem 7.1.3. Visser calls that theorem &quot;truly heavy.&quot; See also <a href="https://www.jstor.org/stable/2586818" rel="nofollow noreferrer">V. Morley's review of Peretyat'kin's book</a>.</p>
<p><em>(An earlier version of this answer omitted Hanf's result; I only found out about it today due to an offhand mention in a different source which, amusingly, I've lost in turn.)</em></p>
<p>Incidentally, the question was first posed by Shoenfield in the final paragraph of his paper <a href="https://www.jstor.org/stable/pdf/2964178" rel="nofollow noreferrer">Degrees of unsolvability associated with classes of formalized theories</a>.</p>

CC BY-SA 4.0
2020-07-15T18:12:50.330Z
2023-07-17T19:11:56.630Z
2023-07-17T19:11:56.630Z
Noah Schweber
<p>I hope that mathematical logic / recursion theory type questions are welcome here. I am sorry this question is so long and technical, but I believe that if you read it you will find that it is well-motivated.</p>
<h1>Definitions</h1>
<ul>
<li>Let <span class="math-container">$a \leq_T b$</span> denote that set <span class="math-container">$a$</span> is Turing reducible to set <span class="math-container">$b$</span>. Additionally, call <span class="math-container">$a$</span> and <span class="math-container">$b$</span> Turing equivalent if <span class="math-container">$a \leq_T b$</span> and <span class="math-container">$b \leq_T a$</span>.</li>
<li>If <span class="math-container">$A$</span> is a set of sentences of first-order logic, let <span class="math-container">$Theory(A)$</span> denote the set of all sentences of first-order logic (FOL) that are logical consequences of <span class="math-container">$A$</span>. If <span class="math-container">$A$</span> is a finite set we say that <span class="math-container">$Theory(A)$</span> is finitely-axiomatizable.</li>
<li>If <span class="math-container">$A$</span> and <span class="math-container">$B$</span> are finite sets of sentences of FOL, then let <span class="math-container">$A \Longrightarrow B$</span> denote that the sentence <span class="math-container">$\land_{a \in A} a$</span> logically implies the sentence <span class="math-container">$\land_{b \in B} b$</span>, or equivalently that <span class="math-container">$Theory(B) \subseteq Theory(A)$</span>.</li>
<li>Let <span class="math-container">$0$</span> denote the Turing degree that contains all decidable sets, and let <span class="math-container">$0'$</span> denote the Turing degree that contains all sets that are Turing equivalent to the set of all pairs <span class="math-container">$(M, x)$</span> such that Turing machine <span class="math-container">$M$</span> halts on input <span class="math-container">$x$</span>.</li>
<li>Let <span class="math-container">$\bot$</span> denote a logically unsatisfiable sentence of FOL, and let <span class="math-container">$\top$</span> denote a logically valid sentence of FOL.</li>
</ul>
<h1>Motivation</h1>
<p>This question is motivated by the similarities between the set of recursively enumerable (r.e.) sets under the Turing-reducibility partial order and the set of sentences of FOL under the logical implication partial order. Here are some connections I noticed:</p>
<ul>
<li><p>For every r.e. set <span class="math-container">$c$</span>, we have that <span class="math-container">$0 \leq_T c \leq_T 0'$</span>. Analogously, for every finite set <span class="math-container">$A$</span> of sentences of FOL, we have that <span class="math-container">$\bot \Longrightarrow A \Longrightarrow \top$</span>.</p>
</li>
<li><p><span class="math-container">$Theory(\bot) \in 0$</span> and <span class="math-container">$Theory(\top)  \in 0'$</span> (This second statement only holds for languages with enough non-logical symbols).</p>
</li>
<li><p>Let <span class="math-container">$A$</span> and <span class="math-container">$B$</span> be finite sets of sentences of FOL. If <span class="math-container">$A \Longrightarrow B$</span>, then <span class="math-container">$Theory(A) \leq_T Theory(B)$</span>.</p>
</li>
</ul>
<p>The third observation can be proven by observing that if <span class="math-container">$A \Longrightarrow B$</span>, then for every sentence <span class="math-container">$C$</span> of FOL, we have that <span class="math-container">$C \in Theory(A)$</span> if and only if <span class="math-container">$A \longrightarrow C \in Theory(B)$</span>, where <span class="math-container">$A \longrightarrow C$</span> is shorthand for <span class="math-container">$\lnot A \lor C$</span>.</p>
<p>These three observations suggest that there are many structural similarities between the r.e. Turing degrees under <span class="math-container">$\leq_T$</span> and the sentences of FOL under <span class="math-container">$\Longrightarrow$</span>. Thus the following question is natural:</p>
<h1>Question</h1>
<p><strong>Is there a language of first-order logic such that every recursively enumerable set is Turing equivalent to a finitely-axiomatizable theory of sentences in that language?</strong></p>
<p>Note that the converse of this question, that every finitely-axiomatizable theory of FOL is Turing equivalent to a recursively enumerable set, is trivially true. Additionally, I can prove this question is true if I remove the requirement that the theory is finitely-axiomatizable.</p>
<p>One problem I've run into is the following. Suppose you are trying to construct a finite set of sentences <span class="math-container">$A$</span> such that <span class="math-container">$Theory(A) \leq_T c$</span>, where <span class="math-container">$c$</span> is a r.e. theory that is strictly 'easier' than the halting problem (i.e. <span class="math-container">$ 0' \not \leq_T c$</span>). Well, <span class="math-container">$Theory(A)$</span> necessarily contains all valid statements (i.e. <span class="math-container">$Theory(\top)$</span>). But <span class="math-container">$Theory(\top)$</span> is Turing equivalent to the halting problem, so we must ensure somehow that <span class="math-container">$Theory(\top)$</span> cannot be recovered from <span class="math-container">$Theory(A)$</span>. I cannot figure out how to ensure this condition.</p>
<p>It is worth noting that the proof of the undecidability of first-order logic given in <em>Computability and Logic</em> by Boolos and Jeffrey only requires a language <span class="math-container">$L$</span> containing the following non-logical symbols: a single constant, four dyadic predicates, and enumerably many monadic predicates.</p>
<h1>Consequences</h1>
<p>If the answer to my question is yes, then I can prove some exciting consequences. Specifically, if the above question is true for a language <span class="math-container">$L$</span> of FOL, then  I can convert statements about Turing degrees into statements about sentences in language <span class="math-container">$L$</span>. I give an example:</p>
<p><strong>Sacks Density Theorem:</strong> If <span class="math-container">$a &lt;_T b$</span>, where <span class="math-container">$a$</span> and <span class="math-container">$b$</span> are r.e. sets, then there is an r.e. set <span class="math-container">$c$</span> such that <span class="math-container">$a &lt;_T c&lt;_T b$</span> (note that <span class="math-container">$a &lt;_T b$</span> means <span class="math-container">$a \leq_T b$</span> and <span class="math-container">$b \not \leq_T a$</span>).</p>
<p>Assuming my question is true for a language <span class="math-container">$L$</span>, I can get the following statement:</p>
<p><strong>Logical Density:</strong> There exists a subset of the set of sentences on <span class="math-container">$L$</span> that is dense under the not logical implication (<span class="math-container">$\not \Rightarrow$</span>) relation.</p>
<p><strong>Proof</strong> (edited for clarity): We build the following set <span class="math-container">$\Gamma$</span> of sentences on <span class="math-container">$L$</span>. For every distinct r.e. Turing degree <span class="math-container">$a$</span>, choose exactly one finite set of sentences <span class="math-container">$A$</span> such that <span class="math-container">$Theory(A)$</span> is Turing equivalent to <span class="math-container">$a$</span>. Convert <span class="math-container">$A$</span> to a single finite sentence by taking the conjunction of each sentence in <span class="math-container">$A$</span>, and add this conjunction to set <span class="math-container">$\Gamma$</span>.</p>
<p>Now we have the following connection between r.e. sets and our set <span class="math-container">$\Gamma$</span>. Consider r.e. sets <span class="math-container">$a$</span> and <span class="math-container">$b$</span> such that <span class="math-container">$a  &lt;_T b$</span>. Then there exists sentences <span class="math-container">$A, B \in \Gamma$</span> such that <span class="math-container">$a$</span> is Turing equivalent to <span class="math-container">$Theory(A)$</span> and <span class="math-container">$b$</span> is Turing equivalent to <span class="math-container">$Theory(B)$</span>. Then by an observation made earlier, this implies that <span class="math-container">$B \not \Rightarrow A$</span> (because if <span class="math-container">$B \Rightarrow A$</span>, then <span class="math-container">$b \leq_T a$</span>, a contradiction). By Sacks density theorem, we must have that there is an r.e. set <span class="math-container">$c$</span> such that <span class="math-container">$a &lt;_T c &lt;_T b$</span>. Then there exists a sentence <span class="math-container">$C \in \Gamma$</span> such that <span class="math-container">$Theory(C)$</span> is Turing equivalent to <span class="math-container">$c$</span>, and by a similar argument as before, <span class="math-container">$B \not \Rightarrow C \not \Rightarrow A$</span>. Now because we've mapped <span class="math-container">$\not \leq_T$</span> to <span class="math-container">$\not \Rightarrow$</span>, a subset of <span class="math-container">$\Gamma$</span> can be chosen that is dense under <span class="math-container">$\not \Rightarrow$</span> (we must choose a subset of <span class="math-container">$\Gamma$</span> that corresponds to a total order of Turing degrees).</p>
<p>There are many results like Sacks theorem that we could convert into statements on sets of sentences in <span class="math-container">$L$</span> if my question was answered affirmatively! It may also be possible to convert statements on sentences in <span class="math-container">$L$</span> to statements on r.e. sets, but this seems harder.</p>
<p>Are there any existing results in the literature that are of a similar flavor to my inquiry?</p>
<p>Thank you for reading!</p>

CC BY-SA 4.0
2020-07-15T14:01:38.373Z
Concerning undecidability of pure first-order logic, it kicks in whenever the language contains at least one at least binary symbol (relation or function), or at least two unary functions (along with equality).
Emil Jeřábek
CC BY-SA 4.0
2020-07-15T14:25:08.843Z
Also, any two languages as above can be suitably translated in each other, hence if the answer to your question is positive for one of them, it is positive for all of them. (Clearly, the answer is negative for the remaining languages, in which all finitely axiomatizable theories are decidable.)
Emil Jeřábek
CC BY-SA 4.0
2020-07-15T14:53:36.700Z
And of course, the "logical density" thing is true: if $A$ is any finitely axiomatized essentially undecidable theory, then the set of sentences implying $A$ modulo logical equivalence, ordered by implication, forms the countable atomless Boolean algebra. (I assume that by "not implying" you actually mean the relation  "$A\Rightarrow B$ and $B\not\Rightarrow A$", as otherwise it's not even transitive.)
Emil Jeřábek
CC BY-SA 4.0
2020-07-15T15:46:46.813Z
Interesting, thank you! I believe that in the example I give, the "not implying" relation (i.e. $B \not \Rightarrow A$) does not include the condition that $A \Rightarrow B$, as it is possible for $a \leq_T b$, but $B \not \Rightarrow A$ where $Theory(A) =_T a$ and  $Theory(B) =_T b$.
Gary Hoppenworth
CC BY-SA 4.0
2020-07-15T15:52:00.967Z
Well, density is a property of partial orders; I've never heard of it being defined for arbitrary relations. But anyway, what you wrote apparently holds in the atomless Boolean algebra as well.
Emil Jeřábek
CC BY-SA 4.0
2020-07-15T16:44:39.477Z
You are right -- there were problems with my original proof. I've edited the proof of that section. I believe if you take a set of of Turing degrees under which $\leq_T$ is a total order, then the $\not \leq_T$ relation is also a total order. Then if you apply the hypothetical construction to convert the r.e. sets to sentences, those sentences will be a total order under the $\not \Rightarrow$ relation.
Gary Hoppenworth
<reference-request><lo.logic><computability>
Is there a language of first-order logic such that every r.e. set is Turing-equivalent to some finitely axiomatizable theory in that language?
Gary Hoppenworth
# Is there a language of first-order logic such that every r.e. set is Turing-equivalent to some finitely axiomatizable theory in that language?

(Asked by: username_0 on 2020-07-15)

I hope that mathematical logic / recursion theory type questions are welcome here. I am sorry this question is so long and technical, but I believe that if you read it you will find that it is well-motivated.

# Definitions

* Let $a \leq\_T b$ denote that set $a$ is Turing reducible to set $b$. Additionally, call $a$ and $b$ Turing equivalent if $a \leq\_T b$ and $b \leq\_T a$.
* If $A$ is a set of sentences of first-order logic, let $Theory(A)$ denote the set of all sentences of first-order logic (FOL) that are logical consequences of $A$. If $A$ is a finite set we say that $Theory(A)$ is finitely-axiomatizable.
* If $A$ and $B$ are finite sets of sentences of FOL, then let $A \Longrightarrow B$ denote that the sentence $\land\_{a \in A} a$ logically implies the sentence $\land\_{b \in B} b$, or equivalently that $Theory(B) \subseteq Theory(A)$.
* Let $0$ denote the Turing degree that contains all decidable sets, and let $0'$ denote the Turing degree that contains all sets that are Turing equivalent to the set of all pairs $(M, x)$ such that Turing machine $M$ halts on input $x$.
* Let $\bot$ denote a logically unsatisfiable sentence of FOL, and let $\top$ denote a logically valid sentence of FOL.

# Motivation

This question is motivated by the similarities between the set of recursively enumerable (r.e.) sets under the Turing-reducibility partial order and the set of sentences of FOL under the logical implication partial order. Here are some connections I noticed:

* For every r.e. set $c$, we have that $0 \leq\_T c \leq\_T 0'$. Analogously, for every finite set $A$ of sentences of FOL, we have that $\bot \Longrightarrow A \Longrightarrow \top$.
* $Theory(\bot) \in 0$ and $Theory(\top) \in 0'$ (This second statement only holds for languages with enough non-logical symbols).
* Let $A$ and $B$ be finite sets of sentences of FOL. If $A \Longrightarrow B$, then $Theory(A) \leq\_T Theory(B)$.

The third observation can be proven by observing that if $A \Longrightarrow B$, then for every sentence $C$ of FOL, we have that $C \in Theory(A)$ if and only if $A \longrightarrow C \in Theory(B)$, where $A \longrightarrow C$ is shorthand for $\lnot A \lor C$.

These three observations suggest that there are many structural similarities between the r.e. Turing degrees under $\leq\_T$ and the sentences of FOL under $\Longrightarrow$. Thus the following question is natural:

# Question

**Is there a language of first-order logic such that every recursively enumerable set is Turing equivalent to a finitely-axiomatizable theory of sentences in that language?**

Note that the converse of this question, that every finitely-axiomatizable theory of FOL is Turing equivalent to a recursively enumerable set, is trivially true. Additionally, I can prove this question is true if I remove the requirement that the theory is finitely-axiomatizable.

One problem I've run into is the following. Suppose you are trying to construct a finite set of sentences $A$ such that $Theory(A) \leq\_T c$, where $c$ is a r.e. theory that is strictly 'easier' than the halting problem (i.e. $ 0' \not \leq\_T c$). Well, $Theory(A)$ necessarily contains all valid statements (i.e. $Theory(\top)$). But $Theory(\top)$ is Turing equivalent to the halting problem, so we must ensure somehow that $Theory(\top)$ cannot be recovered from $Theory(A)$. I cannot figure out how to ensure this condition.

It is worth noting that the proof of the undecidability of first-order logic given in *Computability and Logic* by Boolos and Jeffrey only requires a language $L$ containing the following non-logical symbols: a single constant, four dyadic predicates, and enumerably many monadic predicates.

# Consequences

If the answer to my question is yes, then I can prove some exciting consequences. Specifically, if the above question is true for a language $L$ of FOL, then I can convert statements about Turing degrees into statements about sentences in language $L$. I give an example:

**Sacks Density Theorem:** If $a <\_T b$, where $a$ and $b$ are r.e. sets, then there is an r.e. set $c$ such that $a <\_T c<\_T b$ (note that $a <\_T b$ means $a \leq\_T b$ and $b \not \leq\_T a$).

Assuming my question is true for a language $L$, I can get the following statement:

**Logical Density:** There exists a subset of the set of sentences on $L$ that is dense under the not logical implication ($\not \Rightarrow$) relation.

**Proof** (edited for clarity): We build the following set $\Gamma$ of sentences on $L$. For every distinct r.e. Turing degree $a$, choose exactly one finite set of sentences $A$ such that $Theory(A)$ is Turing equivalent to $a$. Convert $A$ to a single finite sentence by taking the conjunction of each sentence in $A$, and add this conjunction to set $\Gamma$.

Now we have the following connection between r.e. sets and our set $\Gamma$. Consider r.e. sets $a$ and $b$ such that $a <\_T b$. Then there exists sentences $A, B \in \Gamma$ such that $a$ is Turing equivalent to $Theory(A)$ and $b$ is Turing equivalent to $Theory(B)$. Then by an observation made earlier, this implies that $B \not \Rightarrow A$ (because if $B \Rightarrow A$, then $b \leq\_T a$, a contradiction). By Sacks density theorem, we must have that there is an r.e. set $c$ such that $a <\_T c <\_T b$. Then there exists a sentence $C \in \Gamma$ such that $Theory(C)$ is Turing equivalent to $c$, and by a similar argument as before, $B \not \Rightarrow C \not \Rightarrow A$. Now because we've mapped $\not \leq\_T$ to $\not \Rightarrow$, a subset of $\Gamma$ can be chosen that is dense under $\not \Rightarrow$ (we must choose a subset of $\Gamma$ that corresponds to a total order of Turing degrees).

There are many results like Sacks theorem that we could convert into statements on sets of sentences in $L$ if my question was answered affirmatively! It may also be possible to convert statements on sentences in $L$ to statements on r.e. sets, but this seems harder.

Are there any existing results in the literature that are of a similar flavor to my inquiry?

Thank you for reading!

**Tags:** reference-request, lo.logic, computability

> **Comments:**
> **username_1**: Concerning undecidability of pure first-order logic, it kicks in whenever the language contains at least one at least binary symbol (relation or function), or at least two unary functions (along with equality).  
> **username_1**: Also, any two languages as above can be suitably translated in each other, hence if the answer to your question is positive for one of them, it is positive for all of them. (Clearly, the answer is negative for the remaining languages, in which all finitely axiomatizable theories are decidable.)  
> **username_1**: And of course, the "logical density" thing is true: if $A$ is any finitely axiomatized essentially undecidable theory, then the set of sentences implying $A$ modulo logical equivalence, ordered by implication, forms the countable atomless Boolean algebra. (I assume that by "not implying" you actually mean the relation  "$A\Rightarrow B$ and $B\not\Rightarrow A$", as otherwise it's not even transitive.)  
> **username_0**: Interesting, thank you! I believe that in the example I give, the "not implying" relation (i.e. $B \not \Rightarrow A$) does not include the condition that $A \Rightarrow B$, as it is possible for $a \leq_T b$, but $B \not \Rightarrow A$ where $Theory(A) =_T a$ and  $Theory(B) =_T b$.  
> **username_1**: Well, density is a property of partial orders; I've never heard of it being defined for arbitrary relations. But anyway, what you wrote apparently holds in the atomless Boolean algebra as well.  
> **username_0**: You are right -- there were problems with my original proof. I've edited the proof of that section. I believe if you take a set of of Turing degrees under which $\leq_T$ is a total order, then the $\not \leq_T$ relation is also a total order. Then if you apply the hypothetical construction to convert the r.e. sets to sentences, those sentences will be a total order under the $\not \Rightarrow$ relation.  

---

## 1 answers

### Answer by username_2 on 2020-07-15. Score: 13 | Accepted answer

The answer is **yes**.

This was proved by Hanf ([*Model-theoretic methods in the study of elementary logic*, in the **Theory of models** volume](https://www.sciencedirect.com/science/article/abs/pii/B9780720422337500204)). A "uniform" version of this result was conjectured by Hanf and proved by Peretyat'kin in his book [*Finitely axiomatizable theories*](https://rads.stackoverflow.com/amzn/click/com/0306110628); I don't have access to that book, but [Visser's *Essential hereditary undecidability*](https://arxiv.org/pdf/2212.03565.pdf) cites it as Theorem 7.1.3. Visser calls that theorem "truly heavy." See also [V. Morley's review of Peretyat'kin's book](https://www.jstor.org/stable/2586818).

*(An earlier version of this answer omitted Hanf's result; I only found out about it today due to an offhand mention in a different source which, amusingly, I've lost in turn.)*

Incidentally, the question was first posed by Shoenfield in the final paragraph of his paper [Degrees of unsolvability associated with classes of formalized theories](https://www.jstor.org/stable/pdf/2964178).


---

