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?