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.