Ok, yes, yes, I should be marking tripos papers. But I need to take a break before plunging enthusiastically back to reading yet more about gruesome ravens … So, let’s return to Horsten’s paper on ‘Formalizing Church’s Thesis’.
After talking about ‘formalizing’ CT in an intuitionistic framework, Horsten goes on to discuss briefly an analogous shot at formalizing CT in the context of so-called epistemic arithmetic. Now, I didn’t find this very satisfactory as a stand-alone section: but if in fact you first read another paper by Horsten, his 1998 Synthese paper ‘In defense of epistemic arithmetic’, then things do fall into place just a bit better. EA, due originally to Shapiro, is what you get by adding to first order PA an S4-ish modal operator L: and the thought is that this gives a framework in which the classicist can explicitly model something of what the intuitionist is after. So Horsten very briefly explores the following possible analogue of ICT in the framework of EA:
L∀x∃yLAxy → ∃e∀x∃m∃n[T(e, x, m) ∧ U(m, n) ∧ A(x, n)]
But frankly, that supposed analogue seems to me to have very little going for it (for a start, there look to be real problems understanding the modality when it governs an open formula yet is read as being something to do with knowability/informal provability). Horsten’s own discussion seems thoroughly inconclusive too. So I fear that this looks to be an exercise in pretend precision where nothing very useful is going on.
Horsten’s next section on ‘Intensional aspects of Church’s Thesis’ is unsatisfactory in another way. He talks muddily about ‘an ambiguity at the heart of the notion of algorithm’. But there is no such ambiguity. There is the notion of an algorithmic procedure (intensional if you like); and there is the notion of a function in fact being computable by an an algorithmic procedure (so an extensional notion in that, if f has that property, it has it however it is presented). The distinction is clear and unambiguous.
Let’s move on, then, to the next paper, in the Olszewski collection, ‘Remarks on Church’s Thesis and Gödel’s Theorem’ by Stanisław Krajewski. This is too short to be very helpful, so I won’t comment on it — except to say he mentions the unusually overlooked argument from Kleene’s Normal Form Theorem and (a dispensable use of) Church’s Thesis to Gödel’s Theorem that I trailed here. The argument, as Krajewski points out, is due to Kleene himself, a fact which I now realize I didn’t footnote in my book. Oops! I think the book is being printed round about now, so it’s too late to do anything about it. I had better start a corrections page on the web site …