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

Question

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.

Answer 1

I'm not sure why you say "true" is ultimately undefinable, as there is a precise definition for what it means for a first order formula to be true.

What's unique in the case of computability, is that for any definition (as wild as your dreams) for a "computational model", you can finally associate it with a set of functions (the functions it can compute). Thus, you can naturally compare different models, and upon fixing one (based on some empirical justification such as "it is a good representation of computation in the real world") you can call any other model complete if it computes exactly the same set of functions.

However, how do you compare different logics? It seems there is no natural property you can attach to an arbitrary logic, and use it to compare it to other systems. You can perhaps, fix the logic, e.g. first order predicate logic, and ask about completeness of an axiomatic system. Suppose you work in ZFC, and believe it consists of the natural axioms that represent the world. Now, when given a different axiomatic system, you can ask whether they have the same theory, and call this system complete in the case the answer is yes. I think the difference from the computability case, is that for computability, there is a stronger consensus on what the "base model" should be. The reason for this consensus is that many independent models of computation were later shown to be equivalent, so this seems like a very strong empirical evidence for what our "base model" should be.