What is the connection (if any) between proving the undecidability of Robinson Arithmetic and the Church-Turing Thesis? If there is any connection to CTT, is it necessary?

  • I've rolled back the question to its original form - if you want to ask a different question, do so in a separate post rather than radically changing this one. – Noah Schweber Nov 30 '20 at 17:24

There is no connection at all.

CT says that we can interpret the formal result "There is no Turing machine which decides whether a number is the Godel number of a theorem of Q" as "The set of Godel numbers of theorems of Q is not effectively calculable." But this is not relevant to proving that formal result in the first place.

Of course CT does get used all the time in proofs in computability theory, but only in the following way: when we want to argue that a certain operation is computable in the formal sense of Turing machines (or some equivalent model), rather than actually writing down a computation we just describe an algorithm and then say "By CT there's an actual machine which performs this algorithm." But this is only a time-saving technique: we can always sit down and actually write out the desired machine, we're just invoking CT to get out of having to do so (think of it as a really fancy way of saying "The construction of such a machine is left as an exercise for the reader").

So CT is in fact never needed for any proof. It's only ever used to shorten proofs. Its true role comes in interpretation and motivation of theorems and definitions, by connecting formal computation models with the informal-but-compelling notion of effective calculability.

Your Answer

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