Logic Matters

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.

The sixth paper in the Olszewski collection is Jack Copeland’s “Turing Thesis”. Readers who know Copeland’s previous writings in this area won’t be surprised by the general line: but truth trumps novelty, and this is all done with great good sense. To take up a theme in my last posting, Copeland insists that ‘effective’ is a term of art, and that

The Entscheidungsproblem for the predicate calculus [i.e. the problem of finding an effective decision procedure] is the problem of finding a humanly executable procedure of a certain sort, and the fact that there is none is consistent with the claim that some machine may nevertheless be able to decide arbitrary formulae of the calculus; all that follows is that such a machine, if it exists, cannot be mimicked by a human computer.

And he goes on to identify Turing’s Thesis as a claim about what can be done ‘effectively’, meaning by finite step-by-step procedure where each step is available to a cognitive agent of limited (human-like) abilities, etc. Which seems dead right to me (right historically, but also right philosophically in drawing a key conceptual distinction correctly, as I’ve said in previous posts).

Copeland goes on to reiterate chapter and verse from Turing’s writings to verify his reading, and he critically mangles Andrew Hodges’s claims (later in this volume and elsewhere) that Turing originally had a wider thesis about mechanism and also that Turing changed his views after the war about minds and mechanisms. I’m not one for historical minutiae, but Copeland seems clearly to get the best of this exchange.

The next paper is “The Church-Turing Thesis. A last vestige of a failed mathematical program” by Carol E. Cleland. Oh dear. This really is eminently skipable. The first five sections are a lightning (but not at all enlightening) tour through the entirely familiar story of the development of analysis up to Weierstrass, Dedekind and Cantor, the emergence of a set theory as a foundational framework, the ‘crisis’ engendered by the discovery of the paradoxes, Hilbert’s formalizing response, the Entscheidungsproblem as a prompt to the development of a theory of effective computation. No one likely to be reading the Olszewski collection needs the story rehearsing again at this naive level.

And when Cleland comes to the Church-Turing Thesis she without comment runs together two importantly different ideas. On p. 133 the claim is [A] one about the ‘effectively computable’ numerical functions — which indeed is the version of the Thesis relevant to the Entscheidungsproblem. But by p. 140 the Thesis is being read as a claim [B] about the functions which are ‘computable (by any means)’. And these are of course distinct claims, requiring distinct arguments. For example, suppose you think that the kind of hypercomputation that exploits Malament-Hogarth spacetimes is in principle possible: then, on that view, there indeed can be computations which are not effective in the standard sense as explicated e.g. by Hartley Rogers, i.e. involving algorithmic procedures which terminate after some finite number of steps. And the questions we can raise about the Hogarth argument are highly relevant to [B] but not to [A].

Cleland’s last section offers some weak remarks about whether computation ‘by any means’ goes beyond Turing computability; but (I’m afraid) nothing here seriously advances discussion of that topic.

The third, short, paper in the Olszewski collection is by Douglas S. Bridges — the author, with Fred Richman, of the terrific short book Varieties of Constructive Analysis. The book tells us a bit about what happens if you in effect add an axiom motivated by Church’s Thesis to Bishop-style constructive analysis. This little paper says more on the same lines, but I don’t know enough about this stuff to know how novel/interesting this is.

The fourth paper is “On the Provability, Veracity, and AI-Relevance of the Church-Turing Thesis” by Selmer Bringsjord and Konstantine Arkoudas. At least these authors get it right about what the core Thesis is: a numerical function is effectively computable if and only if it is Turing-computable. But that’s about as good as it gets. The first main section is a bash against Mendelson’s argument against “the standard conception of the thesis as mathematically unprovable”. Now, although I am sympathetic to Mendelson’s conclusion, I’d want to argue for it in a rather different way (and do so in the Gödel book). But Bringsjord and Arkoudas’s objections just seem badly point-missing about the possibility of a Mendelsonian line. Their argument (p. 69) depends on a bald disjunction between proofs in formal systems and what they call “empirical evidence” for CTT. But of course, tertium datur. Take, for example, the familiar theorem that there are effectively computable functions which aren’t primitive recursive. I’m not being tendentious in calling that a theorem — that’s how the textbooks label the result. And the textbooks, of course, give a proof using a diagonalization argument. And it is a perfectly good proof even though it involves the informal notion of an effectively computable function (the argument isn’t a fully formalizable proof, in the sense that we can’t get rid of the informal notions it deploys, but it doesn’t just give “empirical” support either). Now, the Mendelsonian line is — I take it — precisely to resist that dichotomy formal/formalizable proof vs mere quasi-empirical support and to remind us that there are perfectly good informal proofs involving informal concepts (and Mendelson invites us to be sceptical about whether the informal/formal division is in fact as sharp as we sometimes pretend). And the key question is whether it is possible to give an informal mathematical proof of CTT as compelling as the proof that not all effectively computable functions are primitive recursive. Reiterating the rejected dichotomy is of course no argument against that possibility.

That’s not a great start to the paper (though the mistake is a familiar one). But things then go further downhill. For much of the rest of the paper is devoted to a discussion of Bringsjord’s claim that membership of “the set of all interesting stories” (!!) is effectively decidable but not recursively decidable (Gödel number the stories and we’d have a counterexample to CTT). And what, according to Bringsjord, is the rationale behind the claim that members of that set is effectively decidable? “The rationale is simply the brute fact that a normal, well-adjusted human computist can effectively decide [membership]. Try it yourself!” Well, you might be able to decide in many cases (always? just how determinate is the idea of an interesting story?): but who says that it is by means of implementing a step-by-step algorithm? Effective decidability is a term of art! It doesn’t just mean there is some method or other for deciding (as in: ask Wikipedia or use a cleverly tuned neural net). It means that there is an algorithmic procedure of a certain sort; and in trying to judge whether a story is interesting it most certainly isn’t available to inspection whether I’m implementing a suitable algorithm. This whole discussion just seems badly misguided.