10
$\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$
  • 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$ – Emil Jeřábek Jul 15 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$ – Emil Jeřábek Jul 15 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$ – Emil Jeřábek Jul 15 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$ – Gary Hoppenworth Jul 15 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$ – Emil Jeřábek Jul 15 at 15:52
8
$\begingroup$

If recollection serves the answer is yes, although it is definitely not easy (so far as I know). The question was first posed by Shoenfield in the final paragraph of his paper Degrees of unsolvability associated with classes of formalized theories. I believe it was first answered by Peretyat'kin, who has proved a number of deep results about the model- and computability-theoretic properties of finitely axiomatized theories (see this review of Peretyat'kin's book); however, I don't have access to the relevant papers at the moment to make certain of things.

| cite | improve this answer | |
$\endgroup$
  • 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$ – Andrej Bauer Jul 16 at 13:52
  • 2
    $\begingroup$ @AndrejBauer I second that request. $\endgroup$ – Noah Schweber Jul 16 at 14:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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