# Is there a dual concept to "Turing Complete" in logic?

Two computing models can be shown to be co complete if each can encode a universal simulator for the other. Two logics can be shown to be co complete if an encoding of the rules of inferences (and maybe axioms if present) of each be shown to be theorems of the other. In computability this has led to a natural idea of Turing completeness and the Church Turing Thesis. However, I have not seen where the logical co completenesses has led to any naturally induced idea of total completeness of similar quality.

Since Provability and Computability are so closely related, so I think it isn't too much to consider that there could be a concept in logic that is a natural dual to Turing Completeness. Speculatively, something like: there is a "true" theorem that isn't provable in a logic if and only if there is a computable function that isn't describable by a computing model. My question is, has anyone studied this? A reference or some keywords would be helpful.

By "true" and "computable" in the previous paragraph I'm referring to the intuitive but ultimately undefinable ideas. For example, someone could show that the finiteness of Goodstein sequences is "true" but not provable in Peano arithmetic without fully defining the concept of "true". Similarly, by diagonalization it can be shown that there are computable functions that are not primitive recursive without actually fully defining the concept of computable. I was wondering, even though they tend to ultimately be empirical concepts, perhaps the concepts could be related to each other well enough to relate the concepts of completeness.

• Interesting post. I wonder how can we show "there are computable functions that are not primitive recursive without actually fully defining the concept of computable". Shouldn't we first well-define the concept "computable" in order to operate with it? Or am I missing something? Commented Jul 20, 2017 at 17:56
• @fade2black If you enumerate all primitive recursive functions as $P$, then define the function $R(x) = P_x(x) + 1$, then $R$ is clearly computable in the intuitive sense but not primitive recursive as it differs from each $P$. The intuitive notion of "I can compute that" was used without actually establishing a computable model. Commented Jul 20, 2017 at 18:11
• Sorry, I meant "computable function". Usually when we say a function $f$ is computable we mean that we have fixed some computable model and there is well-defined set of instructions that on input $x$ gives $f(x)$. Isn't that precise? Commented Jul 20, 2017 at 18:17
• You cannot define away this question. Commented Jul 20, 2017 at 23:06
• Check out Homotopy type theory. Commented Jul 21, 2017 at 18:17