We study the effective versions of several notions related to incompleteness, undecidability, and inseparability along the lines of Pour-El’s insights. Firstly, we strengthen Pour-El’s theorem on the equivalence between effective essential incompleteness and effective inseparability. Secondly, we compare the notions obtained by restricting that of effective essential incompleteness to intensional finite extensions and extensional finite extensions. Finally, we study the combination of effectiveness and hereditariness, and prove an adapted version of Pour-El’s result for this combination.

Kristiansen and Murwanashyaka recently proved that Robinson arithmetic, Q, is interpretable in an elementary theory of full binary trees, T. We prove that, conversely, T is interpretable in Q by producing a formal interpretation of T in an elementary concatenation theory QT+, thereby also establishing mutual interpretability of T with several well-known weak essentially undecidable theories of numbers, strings, and sets. We also introduce a “hybrid” elementary theory of strings and trees, WQT*, and establish its mutual interpretability with Robinson’s weak arithmetic R, the weak theory of trees WT of Kristiansen and Murwanashyaka, and the weak concatenation theory WTCε of Higuchi and Horihata.

In this paper, we examine the limit of applicability of Gödel’s first incompleteness theorem ($\textsf {G1}$ for short). We first define the notion “$\textsf {G1}$ holds for the theory $T$”. This paper is motivated by the following question: can we find a theory with a minimal degree of interpretation for which $\textsf {G1}$ holds. To approach this question, we first examine the following question: is there a theory T such that Robinson’s $\mathbf {R}$ interprets T but T does not interpret $\mathbf {R}$ (i.e., T is weaker than $\mathbf {R}$ w.r.t. interpretation) and $\textsf {G1}$ holds for T? In this paper, we show that there are many such theories based on Jeřábek’s work using some model theory. We prove that for each recursively inseparable pair $\langle A,B\rangle $, we can construct a r.e. theory $U_{\langle A,B\rangle }$ such that $U_{\langle A,B\rangle }$ is weaker than $\mathbf {R}$ w.r.t. interpretation and $\textsf {G1}$ holds for $U_{\langle A,B\rangle }$. As a corollary, we answer a question from Albert Visser. Moreover, we prove that for any Turing degree $\mathbf {0}< \mathbf {d}<\mathbf {0}^{\prime }$, there is a theory T with Turing degree $\mathbf {d}$ such that $\textsf {G1}$ holds for T and T is weaker than $\mathbf {R}$ w.r.t. Turing reducibility. As a corollary, based on Shoenfield’s work using some recursion theory, we show that there is no theory with a minimal degree of Turing reducibility for which $\textsf {G1}$ holds.