10
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – fade2black Jul 20 '17 at 17:56
  • $\begingroup$ @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. $\endgroup$ – DanielV Jul 20 '17 at 18:11
  • $\begingroup$ 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? $\endgroup$ – fade2black Jul 20 '17 at 18:17
  • $\begingroup$ You cannot define away this question. $\endgroup$ – DanielV Jul 20 '17 at 23:06
  • $\begingroup$ Check out Homotopy type theory. $\endgroup$ – Pål GD Jul 21 '17 at 18:17
1
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ There are ways of comparing logics, it just seems you're not aware of them. $\endgroup$ – Andrej Bauer Jul 22 '17 at 9:29
  • $\begingroup$ Guess I should have been more careful. Care to give a more precise answer? $\endgroup$ – Ariel Jul 22 '17 at 9:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.