16
$\begingroup$

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!

$\endgroup$
6
  • 1
    $\begingroup$ 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). $\endgroup$ Jul 15, 2020 at 14:01
  • 1
    $\begingroup$ 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.) $\endgroup$ Jul 15, 2020 at 14:25
  • 2
    $\begingroup$ 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.) $\endgroup$ Jul 15, 2020 at 14:53
  • $\begingroup$ 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$. $\endgroup$ Jul 15, 2020 at 15:46
  • 1
    $\begingroup$ 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. $\endgroup$ Jul 15, 2020 at 15:52

1 Answer 1

13
$\begingroup$

The answer is yes.

This was proved by Hanf (Model-theoretic methods in the study of elementary logic, in the Theory of models volume). A "uniform" version of this result was conjectured by Hanf and proved by Peretyat'kin in his book Finitely axiomatizable theories; I don't have access to that book, but Visser's Essential hereditary undecidability cites it as Theorem 7.1.3. Visser calls that theorem "truly heavy." See also V. Morley's review of Peretyat'kin's book.

(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.

$\endgroup$
4
  • 3
    $\begingroup$ I kindly ask for someone to update the answer with a more precise reference, once they get hold of the relevant papers. $\endgroup$ Jul 16, 2020 at 13:52
  • 2
    $\begingroup$ @AndrejBauer I second that request. $\endgroup$ Jul 16, 2020 at 14:29
  • 2
    $\begingroup$ @AndrejBauer Very belatedly, I've found (via Visser) a source! Still don't have P's book though. $\endgroup$ Dec 8, 2022 at 3:42
  • 1
    $\begingroup$ @AndrejBauer Turns out I was wrong about the citation - Hanf did it before Peretyat'kin, but P's result was stronger. $\endgroup$ Jul 17, 2023 at 23:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.