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.
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:
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.
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!
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
Get help from others!
Recent Answers
Recent Questions
© 2024 TransWikia.com. All rights reserved. Sites we Love: PCI Database, UKBizDB, Menu Kuliner, Sharing RPP