The acceptability of the use of the Church-Turing thesis in mathematical proofs

This small article by Dan Polansky looks into the acceptability of the use of the Church-Turing thesis in mathematical proofs in theoretical computer science. Some of these proofs can be characterized as a "proof by Church's thesis".

The initial consideration or complaint is this. The Church-Turing thesis is not a mathematical theorem. It is an empirical hypothesis. There is a strict separation of the epistemology of mathematics and the epistemology of empirical sciences, such as physics. The universal physical laws are never certain; they are open to refutation/falsification by a later experiment. By contrast, mathematical theorems are conclusively proven to be true. To incorporate the the Church-Turing thesis into a mathematical proof as if it was a lemma is to disrupt the purely mathematical character of the proof. It opens the proof to a risk of later refutation: should someone succeed to refute the Church-Turing thesis (and why should not they, given it is an empirical hypothesis), the refutation is going to impact all the putatively mathematical proofs that depend on it. Formally, this is an unacceptable state of affairs. The resulting enterprise cannot be certified as mathematical; the proofs are not math-worthy. (This is a pun on airworthiness and certification in aerospace industry; see e.g. "Airworthiness Certification of Aircraft | Federal Aviation Administration".)

That is all fair and nice. But it is extremely impractical. Let us consider the theorem that a set that is recursively enumerable and whose complement is also recursively enumerable is thereby actually recusrive (fully decidable rather than merely semidecidable). The proof is straightforward: there must be a program generating the set and a program generating the complement and all one has to do to obtain the decision procedure is to run them in parallel and soon enough, the input is going to be found either in the output of the first program or the second program. We get that the set is recursive (fully decidable). This tacitly assumes the Church-Turing thesis or something similar. Without it, one would have to proceed as follows. The set is recursively enumerable. Therefore, there exists turing machine T1; and for the complement, there exists Turing machine T2. We will now construct Turing machine T3, including its states, transition rules, etc. It would be extremely laborious. And it is very likely to fail to illuminate anything of interest.

The initial complaint is what I raised with my teachers when I studied computer science at a university. The response to it is what I now think is quite reasonable. But the response points to the distinction between the empirical physics and the allegedly non-empirical mathematics being perhaps not as deep as one thinks, on some level. The statement that, say, theorem T1 was correctly proven by means of proof P1 has in principle certain degree of tentativeness. P1 was verified by mathematicians M1 through Mk, but they could all have been wrong. There some kind of cognitive empirical element even in mathematics. A similar point was made in Imre Lakatos in his Proofs and Refutations. That said, the initially highlihgted epistemic distinction between mathematics and empirical sciences is not to be abolished. Rather, one has to explain why the quasi-empirical character of mathematics does not abolish the distinction. And this story shall also be told. (End of the movie, music by Basil Poledouris playing.)

Further reading

• What's the significance of the Church-Turing Thesis?, math.stackexchange.com
• The Church-Turing Thesis, Stanford Encyclopedia of Philosophy
• Church-Turing Thesis, in Practice by Luca San Mauro, 2018, TU Wien