The Church-Turing Thesis (hereafter, TCT) was perhaps the first philosophical problem connected with logic that I have ever encountered in my life. I recall deciding it as the topic of my high school project (I belonged to a special program in the two last years of high school and a ‘research’ work was required in order to pass), being thrilled by the amount of different themes condensed in it. My formation in formal logic was, to say the least, quite poor: I had learnt a bit of set theory, first-order logic and general computation theory on my own. Nevertheless, having concluded this work, I decided to study mathematics so, in some way, I am indebted to the TCT for allowing myself to discover so many rich ideas in the following years.
What attracted to me the most about the TCT was its status and the possibility of providing a formal proof of it. I recall trying to diagonalize the class of algorithms in a similar way as in the Halting problem (‘could a squeeze argument of some kind work?’ >incidentally: some like Smith have argued that a Kreisel-like argument could work!<). Of course, I failed in this and other vague approaches that I tried (recall that I did not know formal logic at all!). That the TCT should be better considered as an empirical statement has been a matter of great controversy. One should first try to clarify what the key notions involved in the TCT are, for this will determine the kind of proof (if any) that it will admit.
There is a general consensus, however, in the fact that the TCT relates two notions: the formal concept of ‘computation’ (encoded in, for instance, Turing machines) and the informal notion(s?) of ‘mechanical procedure’ or ‘effective method’ or ‘algorithm’. Moreover, the TCT declares that both are equivalent. At a first glance, the TCT seems an empirical or ‘open-ended’ statement: it establishes the correspondence between an informal idea and the way in which we try to capture it, so nothing could prevent us from arriving at an algorithm of which no simulation by a Turing machine is possible. The alternative is that the TCT can be regarded as a mathematical statement, that is, one that could be proven. In the latter case, however, it is clear that one should have some way of totally capturing ‘algorithm’ by some formal notion and therefore it seems that the TCT would replicate itself regarding such notion.
A famous proponent of the first claim is Kleene. In fact, he proposed an inductive argument in support of the TCT: (a) every algorithm has been proven, until now, to be equivalent to some Turing machine specification; (b) every process provided, until now, for obtaining new algorithms from others has been simulated by a Turing machine; (c) every attempt, until now, of defining algorithm has resulted in a computation model equivalent to that of Turing machines. One could relate this view to the physical conception of the TCT; in this very broad sense, one could convince himself that the TCT could fail in the next years.
There have been very famous proponents of the second view, like Gödel and Kripke. Gödel regarded Turing’s analysis as a paradigm of analysis of the primitive notions in logic and mathematics: through a series of philosophical developments (the phenomenological method?) trying to understand the vague concept of algorithm, Turing was capable of arriving at the sharp notion of Turing machine. Incidentally, Gödel thought that a similar procedure would allow us to arrive at new axioms of set theory: the notion of set should be similarly analyzed in order for new axioms to intuitively hold (and hence, for example, decide CH!). Gödel had an accidental influence on Gurevich’s and Dershowitz’s approaches to an axiomatic treatment of algorithm, which have been one of the greatests attempts. Of course, the comment above applies once again: how could one be convinced by their axioms? On the other hand, Kripke’s argument consists in understanding computation as a special case of first-order logic proof; by Gödel’s completeness theorem, a first-order logic proof of a given true statement exists, which may be found by a Turing machine so, in general, computations can be simulated by Turing machines. However, Kripke makes use of a premise which is as exotic-looking as the TCT, namely, what he calls ‘Hilbert thesis’: every mathematical notion can be formalized in first-order logic. (Not all the proponents of the second view have been supporters of the truth of the TCT. Famously, Kalmár is known to have claimed that the TCT is false by providing a counterxample, even when its very nature is, as the TCT itself, not very clear in nature.)
The problem of the status and possible proof of the TCT seems to lie at the heart of the way in which we understand the relationship between formal systems and our intuitive or informal notions. It is more severe in the case of the TCT because it involves the highly practical notion of algorithm (or mechanical procedure, or …). To illustrate how the TCT is so special, consider Kripkenstein’s skeptic argument on rule-following: if we are following a rule, how could we rightfully identify such a rule? Or, alternatively, could we not take our course of action as consistent with many different rules? One paradigmatic case is the application of a formal system or rule. Why should we be following a concrete rule and not other that coincides in enough cases with it? The point is that our behavior when following a rule is consistent with an infinite number of different rules. This seems to work as an argument against the identification of formal and informal notions: we simply have too many diverging formal options to properly say that one of them captures the informal concept in question.
The consequence of this in the case of the TCT is the following: we could be using an algorithm A presumably captured by a Turing machine T, but it could also be that A is captured by T’ instead, etc. More problematic would be applying this skepticism to the very same act of rule-following, that is, not that our activity when following a rule should adjust to such rule but that our ativity in general should adjust to the act of rule-following. In particular, this applies to the act itself of following an algorithm. For instance, one could imagine several different ways of following a rule (resp. an algorithm): how could we so sure about following A to begin with? This seems to show that pure action, taken radically, differs with an algorithm in that an algorithm is the determination or specification of a very concrete action. A Turing machine, similarly, provides such specification too. What could then be the difference between, say, A and T?
What I try to point out is that there is no informal notion that can be made totally explicit and that, in some sense, is of special nature. Of course, it may be argued that the concept of Turing machine is as formal as it gets, so it consists in, say, a series of rules (for the formalist) or specifications (for the realist), while the notion of algorithm is closer to natural laguage. But there is no reason to believe that, in the ordinary, informal specification of an algorithm there is ‘more’ than in another specification. The difference is, perhaps, that the notion of algorithm is formalizable, in the sense that we can try to spell out the explicit determinations of which it consists. But this does not mean that the algorithm fits better the action itself than the Turing machine: both are impositions of certain rules, more or less clear, more or less formal.