On, then, to the tenth paper in Church’s Thesis After 70 Years, Leon Horsten’s ‘Formalizing Church’s Thesis’.

Horsten explores two frameworks in which we can write down what look to be, in some sense, partial ‘formalizations’ of CT. Take first an intuitionistic framework (I’ll comment on the framework of so-called epistemic arithmetic in another post). And consider a claim of the form ∀x∃yAxy. Intuitionistically, Horsten suggests, this “means that there is a method for finding for all x at least one y which can be shown to stand in the relation A to x. And this seems close to asserting that an algorithm exists for computing A.” But then, Church’s Thesis tells us that there should be a recursive function that, given x, will do the job for finding a y such that Axy. So by an appeal to Kleene’s Normal Form Theorem, it might seem that in the intuitionistic framework Church’s Thesis implies this, call it ICT:

∀x∃yAxy → ∃e∀x∃m∃n[T(e, x, m) ∧ U(m, n) ∧ A(x, n)]

where T and U express the familiar p.r. Kleene functions.

Now, Horsten has seemingly sane things to say about why, however, ICT doesn’t really capture CT — and so the common intuitionistic rejection of ICT as too strong isn’t really a strike against CT. But that isn’t a novel thought. What was news to me is a theorem that Horsten credits to Anne Troelstra. Take Heyting Arithmetic plus ICT; then if this proves δ(φ), where this is the double-negation translation of φ, then Peano Arithmetic proves φ. Which is kind of cute. But what is the significance of that? Horsten’s comment is: “This conservativity phenomenon can be seen as a weak form of evidence for the thesis that CT is conservative over classical mathematics.” Why so?

OK, we often argue to some formal conclusion informally, using the assumption that a certain function is computable, and appeal to CT to avoid (i) bothering to prove the function in question is recursive and then (ii) turning our sketched argument into a stricter proof for the same formal conclusion. The assumption is that we can always do away with such an labour-saving appeal to CT: call that, if you like, the assumption that CT is conservative over classical mathematics. But it is equally, of course, the assumption that CT is true. For if CT weren’t conservative, there would be a disconnect between claims about computability and claims about recursiveness and CT would be false. And conversely, if CT were false (in the only way it can be false, by there being a computable but not recursive numerical function) then it wouldn’t be conservative: e.g., trivially, if f were such a function, then an appeal to CT followed by KNFT would deduce a false equivalence between f(x) = y and ∃e&existm[T(e, x, m) ∧ U(m, y)]. So Horsten’s claim comes to this: Troelstra’s theorem is evidence that CT is true.

But is it? After all, suppose the theorem had failed: would that have dented our confidence in CT? Surely not: we’d just have concluded that ICT — which even intuitionists reject as too strong — really is far too strong (compare other cases where wildly optimistic constructivist assumptions can prove classically unacceptable claims, e.g. about the continuity of functions). But if failure of the theorem wouldn’t have dented the classical mathematician’s confidence in CT, in what sense does its success give any kind of evidential boost for CT?

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).