I’m going to pass over the next three papers in the Olszewski collection pretty quickly, for various reasons.

First, there’s a piece on “Analog computation and Church’s Thesis” by Jerzy Mycka: I just don’t know anything about this stuff, and am certainly not in a position to comment on this piece, though it looks decent enough.

Then there is a paper by Piergiorgio Odifreddi on “Kreisel’s Church”. Now, I find Kreisel’s writings intriguing and irritating in roughly equal measure (all sorts of interesting things seem to be going on, but he just can’t or won’t write flat-footed technical exposition and direct, transparent, plain-spoken, philosophical commentary). So I’d hoped that Odifreddi might take up one or two of Kreisel’s themes from his discussions of CT and give them a careful development and exploration — for Odifreddi’s wonderful book on Recursion Theory shows how clear and judicious he can be. But regrettably, he does something quite different: he takes us on a lightening survey of Kreisel’s many relevant articles, with a lot of quotations and some references to related later work. But if you were puzzled by Kreisel before, you’ll stay pretty puzzled — though you’ll have a longer bibliography!

Next, Adam Olszewski contributes a short piece on “Church’s Thesis as interpreted by Church”. Here Olszewski does at least pick up on the point that I noted that Murawski and Wolenski slurred over without comment. CT is nowadays usually taken to be a claim about the co-extensiveness of the two notions of effective computability and recursivess; but the Founding Fathers were wont to talk of the notions being identical, or of one notion being a definition of the other. Church in 1936 himself uses both identity talk and definition talk. But actually, it isn’t too likely that — at that early date — Church had a clearly worked out position in mind on the status of the correlation he was proposing between computability and recursivess, and I don’t think we can read too much into his choice of words here. The headline is that Church, at least originally, seemed to take the modest view of the correlation as having something like the status of a Carnapian explication, while Turing thought, more boldly, that it could be forced on us by an analysis of the very notion of a computation. This is familiar stuff, however, and Olszewski’s brief remarks don’t in any way change the familiar picture.

So, we’re halfway through my blogview of Church’s Thesis After 70 Years edited by Adam Olszewski, Jan Wolenski and Robert Janusz: I’ve commented on eleven papers, and there are eleven to go. I’m afraid that so far I’ve not been wildly enthusiastic: the average level of the papers is not great. But there are cheering names yet to come: Odifreddi, Shapiro, Sieg. So I live in hope …

But the next paper — Charles McCarty’s ‘Thesis and Variation’ — doesn’t exactly raise my spirits either. The first couple of sections are pretentiously written, ill-focused, remarks about ‘physical machines’ and ‘logical machines’ (alluding to Wittgenstein). The remainder of the paper is unclear, badly expounded, stuff about modal formulations of CT (in the same ball park, then, as Horsten). Surely, in this of all areas of philosophy, we can and should demand direct straight talking and absolute transparency: and I’ve not the patience to wade through authors who can’t be bothered to make themselves totally clear.

At least the next piece, five brisk sides by Elliott Mendelson, is clear. He returns to the topic of his well known 1990 paper, and explains again one of his key points:

I do not believe that the distinction between “precise” and “imprecise” serves to distinguish “partial recursive function” from “effectively computable function”.

To be sure, we offer more articulated definitions of the first notion: but, Mendelson insists, we only understand them insofar as we have an intuitive understanding of the notions that occur in the definition. Definitions give out at some point where we are (for the purposes at hand) content to rest: and in the end, that holds as much for “partial recursive function” as for “effectively computable function”

Mendelson’s point then is that the possibility of establishing the ‘hard’ direction of CT can’t be blocked just by saying that the idea of a partial recursive function is precise, the idea of an effectively computable function is isn’t, so that there is some sort of categorial mismatch. (Actually, though I take Mendelson’s point, I’d want stress a somewhat different angle on it. For CT is a doctrine about the co-extensiveness of two concepts. And there is nothing to stop one concept having the same extension as another, even if the first is in some good sense relatively ‘imprecise’ and the second is ‘precise’ — any more than there is anything to stop an ‘imprecise’ designator like “those guys over there” in the circumstances picking out exactly the same as “Kurt, Stephen, and Alonzo”.)

As to the question whether the hard direction can actually be proved, Mendelson picks out Robert Black’s “Proving Church’s Thesis”, Philosophia Mathematica 2000, as the best recent discussion. I warmly agree, and I take up Robert’s story in the last chapter of my book.

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 …