Church’s Thesis 8: Formalizing the thesis

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 ∀xyAxy. 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:

xyAxy → ∃exmn[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?

Good heavens, a decent meal in Cambridge

This won’t be of much interest to my enormous world-wide readership (well, putting a tracker on this blog certainly is a good corrective for any great delusions on that score!), but after the last logic seminar of the academic year a few of us went out to the Rice Boat, a relatively new Indian restaurant very near the faculty, specializing in Kerala cuisine. We all agreed it was simply terrific. Highly recommended.

Hand engraved examination scripts

What strikes me as I wade through Part II tripos papers (well, the thing that strikes me that it wouldn’t be out of place to comment on, here and now) is that students are tending to write less than they used to. And I suspect that part of the explanation is this: few students actually ever write at length by hand any more, from one examination season to the next. Weekly essays are invariably word-processed; note-taking in lectures is a dying art (since people often give copious handouts, and students can then just make short scribbles on those); more and more students take their laptops to the libraries to make notes there. So the business of sitting down for three hours pushing pen across paper, fast and furious, must be an unaccustomed physical challenge, for a start. And it’s no doubt even more of a challenge to compose something straight onto the page in a quite different way to what students are now used to. I certainly wouldn’t like to have to do it.

But of course the shorter an answer, the more difficult it is to shine (especially if an answer starts with a bit of routine exposition). Heaven knows what we do about this: but we are surely — sooner rather than later — going to have to come up with a system that doesn’t quite so favour those who have happened to acquire the philosophically irrelevant antique skill of being able to write fast.

Church’s Thesis 7: Physical computability

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.

Tesco’s shows unexpected taste and discrimination

Wow. Tesco Entertainment is selling my Gödel book. Look for piles by the checkouts when publication arrives! I’m booking a world cruise on the expected sales right now.

And on the same page they are advertising another ‘hot product’ (their words), Carol Vorderman’s Maths Made Easy: Ages 3-5, Preschool Shapes and Patterns. Well, I have tried to make my book reasonably accessible: but I’m not quite so sure the markets will overlap.

I think tripos marking is making me lightheaded.

At last, again …

At long last, the final final version of my Gödel book went to the publishers this afternoon. I’ve been taking advantage of a quite unexpected chance to make changes until the last moment — and I think that some that I’ve made in the last month have been quite significant improvements. But now I really do have to stop. And indeed a pile of tripos papers arrived to mark which will prevent me neurotically worrying about stuff that it is too late to change anyway!

It’s an odd feeling, finally letting go. On the whole,as I’ve said before, I’m pretty pleased with the result. To be sure, if I were starting afresh I’d handle a few things a bit differently; and it will be interesting to see if the few sections that still bug me as being really too skimpy technically or philosophically are the ones which reviewers pick up on. But I’m not sure that I could really have sorted them out without making a long book (already at the limits of CUP’s patience) quite a bit longer. So the book will have to take its chances as is!

Phew! A glass or three of Caol Ila seems in order …

The Symposium

A couple of days ago in an Oxfam shop I picked up a second-hand copy of a beautiful parallel text of the Symposium, with a racy and highly readable translation by Tom Griffith and wonderfully evocative wood engravings by Peter Forster. It’s a fun read (though I found the experience tinged with regret at the more or less total loss of my Greek).

But is it still philosophically important? Philosophical interest is not a timeless feature of a text, it seems. No doubt the Symposium is a great source for those looking for clues about the mores of ancient Athens (and that is a fascinating subject: put James Davidson’s Courtesans and Fishcakes on your reading list if you don’t know that terrific exploration). But does the Symposium really tell you anything serious about its ostensible subject, love? Indeed, how do you ‘philosophize’ about that? Read the English poets instead!

Church’s Thesis 6: Concepts, extensions, and proofs

Continuing my blogview of the papers in Church’s Thesis After 70 Years, I’ll skip the contribution by Hartmut Fitz to return to later, and next look at Janet Folina’s ‘Church’s Thesis and the variety of mathematical justifications’ because I’m interested in her main topic, the variety in the idea of proof (I’m just looking one last time at the concluding few sections of my Gödel book, where I talk about this too).

Folina’s paper, though, gets off on the wrong foot. She writes: “Rather than a claim about mathematical objects such as numbers or sets, CT (insofar as it is an assertion) is a claim about a concept. Assessing it requires conceptual analysis.” Which makes it sound as if arguing about CT is like arguing whether the concept of knowledge can be analysed as the concept of justified true belief. But whatever the history of this, nowadays CT is, precisely, a claim about mathematical objects (in the broad, non-Fregean, sense of ‘object’): it’s the claim that a function is effectively computable if and only if it is recursive — or equivalently, if and only if it is Turing computable. And the truth of that extensional claim doesn’t depend on any claim about whether mere conceptual analysis can reveal e.g. that the effectively computable functions are Turing computable.

(Aside: In fact, it is as clear as anything is in this area that, pace Turing, mere conceptual analysis couldn’t reveal such an equivalence, since there is nothing in the notion of an effective computation that demands that the ‘shape’ of our workspace stays fixed during a computation — quite the contrary, we often throw away scratch working, reassemble pages of a long computation etc. — whereas a Turing machine operates on a fixed workspace. It requires a theorem, not conceptual analysis, to tell us that what is computable in a more dynamically changeable workspace is also Turing computable.)

But as I say, Folina’s main remarks are about the notion of ‘proof’ involved in the majority claim that CT is unprovable, and in the minority claim that it is, or might be, provable. She insists that there can be mathematical reasons for a proposition that aren’t proofs, properly so called. Fair enough. But she seems to have in mind the sort of grounds we might have for believing Goldbach’s conjecture. And it isn’t clear to me what she’d say about e.g. the diagonal argument that there are effectively computable functions which aren’t primitive recursive. This isn’t just a quasi-inductive argument, and we’d indeed normally announce it as a proof even though it doesn’t fall under what Folina calls the “Euclidean” concept of mathematical proof, i.e. “a deductively valid argument in some axiomatic (or suitably well defined) system”, given that it involves the intuitive idea of an effectively computable function.

But say what you like here. For even if we allow Folina to reserve (hijack?) the term ‘proof’ for the “Euclidean” cases, the question remains in place whether there can be an argument for CT which is as rationally compelling as the argument that shows that there are effectively computable functions which aren’t p.r., or whether ultimately the grounds are more like the quasi-inductive reasons that support a belief in Goldbach’s conjecture. And that’s the real issue at stake about the status of CT (not whether we call such an argument, if there is one, a proof).

England in May

Near Newton BlossomvilleOften we think about going to live in Italy in a couple of years or so, but it would be a wrench not to see the wooded English countryside in May (we forgot to take the camera when walking last weekend in a quite unregarded area of Bedfordshire — but it was stunning in its quiet way, as even a phone snap hints).

One of the less welcome delights of May, however, is tripos-marking, which starts for me at the end of this week. And before then, I have the tough task of ranking thirty six applications for the Analysis studentship, many of them impressive. So this blog will probably now slow down a bit after the recent flurry of postings.

Church’s Thesis 5: Effective computability, machine computability

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.

Scroll to Top