Olszewski

The next paper in the Olszewski collection is Wilfried Sieg’s “Step by recursive step: Church’s analysis of effective computability”. And if that title seems familiar, that’s because the paper was first published ten years(!) ago in the Bulletin of Symbolic Logic. I’ve just reread the paper, and the historical fine detail is indeed interesting, but not (I think) particularly exciting if your concerns are about the status of Church’s Thesis now the dust has settled. So, given that the piece is familiar, I don’t feel moved to comment on it further here.

Sieg’s contribution is disappointing because it is old news; the last two papers are disappointing because neither says anything much about Church’s Thesis (properly understood as a claim about the coextensiveness of the notions of effective computability and recursiveness). Karl Svozil, in “Physics and Metaphysics Look at Computation”, instead writes about what physical processes can compute, and in particular says something about quantum computing (and says it too quickly to be other than fairly mystifying). And David Turner’s “Church’s Thesis and Functional Programming” really ought to be called “Church’s Lambda Calculus and Functional Programming”.

Which brings us to the end of the collection. A very disappointing (at times, rather depressing) read, I’m afraid. My blunt summary suggestion: read the papers by Copeland, Shagrir, and Shapiro and you can really give the other nineteen a miss …

Back at last to my blogview of the papers in Church’s Thesis After 70 Years (new readers can start here!) — and we’ve reached a very nice paper by Stewart Shapiro, “Computability, Proof, and Open-Texture”, written with his characteristic clarity and good sense. One of the few ‘must read’ papers in the collection.

But I suspect that Shapiro somewhat misdescribes the basic logical geography of the issues in this area: so while I like many of the points he makes in his paper, I don’t think they support quite the conclusion that he draws. Let me explain.

There are three concepts hereabouts that need to be considered. First, there is the inchoate notion of what is computable, pinned down — in so far as it is pinned down — by examples of paradigm computations. Second, there is the idealized though still informal notion of effective computability. Third, there is the notion of Turing computability (or alternatively, recursive computability).

Church’s Thesis is standardly taken — and I’ve been taking it — to be a claim about the relation between the second and third concepts: they are co-extensive. And the point to emphasize is that we do indeed need to do some significant pre-processing of our initial inchoate notion of computability before we arrive at a notion, effective computability, that can reasonably be asserted to be co-extensive with Turing computability. After all, ‘computable’ means, roughly, ‘can be computed’: but ‘can’ relative to what constraints? Is the Ackermann function computable (even though for small arguments its value has more digits than particles in the known universe)? Our agreed judgements about elementary examples of common-or-garden computation don’t settle the answer to exotic questions like that. And there is an element of decision — guided of course by the desire for interesting, fruitful concepts — in the way we refine the inchoate notion of computability to arrive at the idea of effective computability (e.g. we abstract entirely away from consideration of the number of steps needed to execute an effective step-by-step computation, while insisting that we keep a low bound on the intelligence required to execute each particular step). Shapiro writes well about this kind of exercise of reducing the amount of ‘open texture’ in an inchoate informal concept and arriving at something more sharply bounded.

However, the question that has lately been the subject of some debate in the literature — the question whether we can give an informal proof of Church’s Thesis — is a question that arises after an initial exercise of conceptual refinement has been done, and we have arrived at the idea of effective computability. Is the next move from the idea of effective computability to the idea of Turing computability (or some equivalent) another move like the initial move from the notion of computability to the idea of effective computability? In other words, does this just involve further reduction in open texture, guided by more considerations ultimately of the same kind as are involved in the initial reduction of open texture in the inchoate concept of computability (so the move is rendered attractive for certain purposes but is not uniquely compulsory). Or could it be that once we have got as far as the notion of effective computability — informal though that notion is — we have in fact imposed sufficient constraints to force the effectively computable functions to be none other than the Turing computable functions?

Sieg, for example, has explored the second line, and I offer arguments for it in my Gödel book. And of course the viability of this line is not in the slightest bit affected by agreeing that the move from the initial notion of computability to the notion of effective computability involves a number of non-compulsory decisions in reducing open texture. Shapiro segues rather too smoothly from discussion of the conceptual move from the inchoate notion of computability to the notion of effective computability to discussion of the move from effective computability to Turing computability. But supposing that these are moves of the same kind is in fact exactly the point at issue in some recent debates. And that point, to my mind, isn’t sufficiently directly addressed by Shapiro in his last couple of pages to make his discussion of these matters entirely convincing.

But read his paper and judge for yourself!

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 …

As light relief from tripos marking, back to commenting on two more papers in the Olszewski collection: “Church’s Thesis and physical computation” by Hartmut Fitz, and “Did Church and Turing have a thesis about machines?” by Andrew Hodges. But I’ll be very brief (and not very helpful).

Both papers are about what Fitz calls the Physical Church-Turing Thesis (a function is effectively computable by a physical system iff it is Turing machine computable), and its relative the Machine Church-Turing Thesis (a function is effectively computable by a machine iff it is Turing machine computable). Hodges argues that the founding fathers, as a matter of historical fact, endorsed MCT. I’ve already noted, though, that Copeland in his piece has vigorously and rather convincingly criticized Hodges’s line, and I’ve nothing more to add.

Fitz, however, isn’t so much interested in the historical question as in the stand-alone plausibility of MCT and PCT. He covers a lot of ground very fast in his discussion: some of what he says I found obscure, some points look good ones but need more development, and I’m not sure I’m getting a clear overall picture. But in any case, I can’t myself get very worked about MCT and PCT once we’ve granted that neither is implied by the core Church-Turing Thesis, so I’m probably not paying Fitz quite enough attention. Anyway, I’m cheerfully going to skip on to the next papers.