TransWikia.com

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?

Theoretical Computer Science Asked by Gary Hoppenworth on October 30, 2021

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!

One Answer

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.

Answered by Noah Schweber on October 30, 2021

Add your own answers!

Ask a Question

Get help from others!

© 2024 TransWikia.com. All rights reserved. Sites we Love: PCI Database, UKBizDB, Menu Kuliner, Sharing RPP