Continuing my blogview of the papers in Church’s Thesis After 70 Years, I’ll skip the contribution by Hartmut Fitz to return to later, and next look at Janet Folina’s ‘Church’s Thesis and the variety of mathematical justifications’ because I’m interested in her main topic, the variety in the idea of proof (I’m just looking one last time at the concluding few sections of my Gödel book, where I talk about this too).

Folina’s paper, though, gets off on the wrong foot. She writes: “Rather than a claim about mathematical objects such as numbers or sets, CT (insofar as it is an assertion) is a claim about a concept. Assessing it requires conceptual analysis.” Which makes it sound as if arguing about CT is like arguing whether the concept of knowledge can be analysed as the concept of justified true belief. But whatever the history of this, nowadays CT is, precisely, a claim about mathematical objects (in the broad, non-Fregean, sense of ‘object’): it’s the claim that a function is effectively computable if and only if it is recursive — or equivalently, if and only if it is Turing computable. And the truth of that extensional claim doesn’t depend on any claim about whether mere conceptual analysis can reveal e.g. that the effectively computable functions are Turing computable.

(Aside: In fact, it is as clear as anything is in this area that, pace Turing, mere conceptual analysis couldn’t reveal such an equivalence, since there is nothing in the notion of an effective computation that demands that the ‘shape’ of our workspace stays fixed during a computation — quite the contrary, we often throw away scratch working, reassemble pages of a long computation etc. — whereas a Turing machine operates on a fixed workspace. It requires a theorem, not conceptual analysis, to tell us that what is computable in a more dynamically changeable workspace is also Turing computable.)

But as I say, Folina’s main remarks are about the notion of ‘proof’ involved in the majority claim that CT is unprovable, and in the minority claim that it is, or might be, provable. She insists that there can be mathematical reasons for a proposition that aren’t proofs, properly so called. Fair enough. But she seems to have in mind the sort of grounds we might have for believing Goldbach’s conjecture. And it isn’t clear to me what she’d say about e.g. the diagonal argument that there are effectively computable functions which aren’t primitive recursive. This isn’t just a quasi-inductive argument, and we’d indeed normally announce it as a proof even though it doesn’t fall under what Folina calls the “Euclidean” concept of mathematical proof, i.e. “a deductively valid argument in some axiomatic (or suitably well defined) system”, given that it involves the intuitive idea of an effectively computable function.

But say what you like here. For even if we allow Folina to reserve (hijack?) the term ‘proof’ for the “Euclidean” cases, the question remains in place whether there can be an argument for CT which is as rationally compelling as the argument that shows that there are effectively computable functions which aren’t p.r., or whether ultimately the grounds are more like the quasi-inductive reasons that support a belief in Goldbach’s conjecture. And that’s the real issue at stake about the status of CT (not whether we call such an argument, if there is one, a proof).

This series on the Church’s Thesis book has been rather interesting. I was wondering if you could say a little more about how a dynamically changing workspace affects computation. Turing machines have a fixed (infinite) tape, but they can erase old data and overwrite parts of the tape, which doesn’t seem different than, say, adding more tape. Do you have in mind the case where the work space is finite (and possibly relatively limited)?

Well, a dynamically changing workspace could involve more than just “adding more tape” (at one or other end of the occupied cells); we could imagine changing the topology of the workspace (e.g. temporarily gluing together “edges” of the workspace, and so on).

However, allowing these more radical changes doesn’t in fact change what is computable. Whatever is Kolmogorov-Uspenskii computable (computable in a dynamically changing work) is Turing computable. Perhaps there are relevant speed-up theorems, but the class of computable functions stays the same. I was noting, however, that this is a mathematical theorem — something that needs mathematical argument to establish rather than something to be revealed by “conceptual analysis”.