One True Logic

There’s a new book out by Owen Griffiths and Alex Paseau, One True Logic: A Monist Manifesto (OUP). As the title suggests, this argues against logical pluralism. Yes, of course, there are myriad logical systems which we can concoct and study as interesting mathematical objects. But what about the logic we actually use in reasoning about them and about other mathematical matters? Is there in fact one correct logic which tracks what really does follow from what? Our authors take a conservative line, in that they are anti-pluralist: there is indeed one true logic for in-earnest applications. They are unconservative in defending a highly infinitary logic in that role.

I’ve read the first few chapters with enjoyment and enlightenment. But I’m going to have to shelve the book for the moment, as it will be too distracting from other commitments to engage seriously with the rest of it for a while. One of the delights of somewhat senior years is finding it more difficult to think about more than one thing at a time. (“But what’s new?” murmurs Mrs Logic Matters from the wings.)

For a start, I must continue cracking on with the category theory project. I have now revised Chapters 1 to 15 of Beginning Category Theory. So here they are, in one long PDF which also includes the remaining unrevised chapters from the 2015/2018 Gentle Intro.

In this iteration there are quite a few minor changes to Chapters 1 to 13 (correcting typos, clarifying some phrasing, deleting an unnecessary section, adding a new theorem in §12.2, etc.), though there is nothing very significant there. I have also now revised Chapter 15, the first of the two general chapters on limits/colimits. This and the preceding chapter on equalisers/co-equalisers could surely do with more polishing and lightening-up in places. But as I’ve said previously, I’m including revised chapters when they are at least an improvement on what went before (I’m not waiting for final-draft perfection!).

If you are like me, you are looking for the more-than-occasional consoling distractions from the state of the wider world. Let me share one.

Of the great pianists I have had the chance to hear live over the years, the one I perhaps find the most emotionally engaging of all is Maria João Pires. Her unmannered directedness goes straight to the heart. So here she is, playing Schubert, Debussy and Beethoven, in a video recorded in Gstaad last August.

Not Thinking Like a Liberal

For over ten years, Raymond Geuss and I were both members of the Cambridge Philosophy Faculty. But apart from one year when, like two unbelieving bishops, we had to co-examine a metaphysics paper, I doubt we spoke more than a few hundred words. I suspect he thought I was simply an uninteresting unphilosophical philistine. In fact, we might have had just a little more in common than he suspected, apart from contrarian tendencies — stretching from being both brought up as Catholics to both being amused by the racier ancient Greek epigrams (indeed the first things I ever read by him were his versions in his Parrots, Poets, Philosophers and Good Advice).

I have now just been reading Geuss’s new and very personal short book Not Thinking Like a Liberal (Harvard UP) with great enjoyment and some enlightenment too. He starts by recounting his strange out-of-its-time education, at a Catholic boarding school in the USA, largely staffed by Piarist priests, many Hungarian emigrés. This taught not a narrow authoritarian Catholicism, but a wide-ranging European culture transplanted to Pennsylvania. And Geuss finds — especially in the remembered teaching of one Fr. Krigler — the roots of his own distancing from the shallow “liberalism” of the kind he discerns in much political thinking. The earlier parts of the book are indeed fascinating and insightful.

Later pages found me a bit less carried along. Geuss does no better than others, for example, in conveying what was supposed to be so impressive about his teacher Sydney Morgenbesser at Columbia (Morgenbesser sounds pretty irritating to me). And the concluding pages about unclarity are rather too arm-waving, and the pages about negativity rather too negative, for my liking. But I still very warmly recommend this book as perhaps the most engaging of his writings (apart from those epigrammatic poems, that is!). It got me thinking about scripture and religious traditions, about authority, about education … and about liberalism and the tenor of our times.

Juliette Kennedy, Gödel’s Incompleteness Theorems

I was in the CUP Bookshop the other day, and saw physical copies of the Elements series for the first time. I have to say that the books are suprisingly poorly produced, and very expensive for what they are. I suspect that the Elements are primarily designed for online reading; and I certainly won’t be buying physical copies.

I’ve now read Juliette Kennedy’s contribution on Gödel’s Incompleteness Theorems. Who knows who the reader is supposed to be? It is apparently someone who needs the notion of a primitive recursive function explained on p. 11, while on p. 24 we get a hard-core forcing argument to prove that “There is no Borel function F(s) from infinite sequences of reals to reals such that if ran(s) = ran(s’), then F(s) = F(s’), and moreover F(s) is always outside ran(s)” (‘ran’ isn’t explained). This is just bizarre. What were the editors of this particular series thinking?

Whatever the author’s strengths, they don’t include the knack of attractive exposition. So I can’t recommend this for reading as a book. But if you already know your way around the Gödelian themes, you could perhaps treat this Element as an occasionally useful scrapbook to dip into, to follow up various references (indeed, some new to me). And I’ll leave it at that.

Birthday treats

Another birthday yesterday, a quite daft number, but much better than the alternative. A few treats, and two of them anyone else can enjoy too for a relatively modest outlay. One was the book accompanying the new Raphael exhibition at the National Gallery. Will we brave the covid-ridden crowds to go up to the exhibition ourselves? As asking the question that way suggests, I rather doubt it. But the catalogue book, as nearly always for the National  Gallery’s major events, is pretty terrific, and will be a lasting pleasure in itself. And the DVD of the 2020 Salzburg Festival Così fan Tutte which we watched last night is just a delight. Hugely enjoyable, very engagingly acted, with some wonderful singing, in particular from Elsa Dreisig. So both the book and the DVD are very warmly recommended; we all need cheering.

Greg Restall, Proofs and Models in Philosophical Logic

I notice that Juliette Kennedy’s book on Gödel’s incompleteness theorems in the Cambridge Elements series has now also been published. I’ll no doubt get round to commenting on that in due course, along with John Bell’s short book on type theory. But first, let me say something about Greg Restall’s contribution to the series: as I said, for the coming few days you can freely download a PDF here.

There does seem little consistency in the level/intended audience of the various books in this series. As we will see, Bell’s book is pretty hard-core graduate level, and mathematical in style and approach. Burgess’s book I found to be a bit of a mixed bag: the earlier sections are nicely approachable at an introductory level; but the later overview of topics in higher set theory — though indeed interesting and well done — seems written for a different, significantly more mathematically sophisticated, audience. It is good to report, then, that Greg Restall — as his title promises — does keep philosophers and philosophical issues firmly in mind; he writes with great clarity at a level that should be pretty consistently accessible to someone who has done a first formal logic course.

After a short scene-setting introduction to the context, there are three main sections, titled ‘Proofs’, ‘Models’ and ‘Connections’. So, the first section is predictably on proof-styles — Frege-Hilbert proofs, Gentzen natural deduction, single-conclusion sequent calculi, multi-conclusion sequent calculi — with, along the way, discussions of ‘tonk’, of the role of contraction in deriving certain paradoxes, and more. I enjoyed reading this, and it strikes me as extremely well done (a definite recommendation for motivational reading in the proof-theory chapter of the Beginning Math Logic guide).

I can’t myself muster quite the same enthusiasm for the ‘Models’ section — though it is written with the same enviable clarity and zest. For what we get here is a discussion of variant models (at the level of propositional logic) with three values, with truth-value  gaps, and truth-value gluts, and with (re)-definitions of logical consequence to match, discussed with an eye on the treatment of various paradoxes (the Liar, the Curry paradox, the Sorites). I know there are many philosophers who get really excited by this sort of thing. Not me. However, if you are one, then you’ll find Restall’s discussion a very nicely organized introductory overview.

The shorter ‘Connections’ section, as you’d expect, says something technical about soundness and completeness proofs; but it also makes interesting remarks about the philosophical significance of such proofs, depending on whether you take a truth-first or inferentialist approach to semantics. (And then this is related back to the discussion of the paradoxes.)

If you aren’t a paradox-monger and think that truth-value gluts and the like are the work of the devil, you can skim some bits and still get a lot out of reading Restall’s book. For it is always good to stand back and see an area — even one you know quite well — being organised by an insightful and eminently clear logician. Overall, then, an excellent and very welcome Element.

John Burgess, Set Theory

Of making many logic books there is no end. So a project like the Beginning Mathematical Logic study guide has no terminus. I hit the “pause” button at an arbitrary moment, and published the first book edition a couple of months ago, because I wanted to concentrate for a while on other things. But needless to say, there are already a number of new publications which are possible candidates for being mentioned in the next edition. In particular there are the four first books in the Cambridge Elements series on Philosophy and Logic. Three have already been published — in fact, the first of them just as I was finishing the guide, namely John Burgess’s Set Theory. Then we have John Bell on Higher-Order Logic and Type Theory, and Greg Restall on Proofs and Models in Philosophical Logic. Juliette Kennedy’s Gödel’s Incompleteness Theorems is due any day. The first three should already be accessible, then, via Cambridge Core if your library has a subscription; and even better, Proofs and Models is free to download here for another week. I’ll try to say something brief about each of these books over the coming days.

First then Burgess on sets. Like other Elements, this little book is about seventy, not-very-packed, pages (perhaps 30K words?). More than an encyclopedia article, or a handbook chapter, but half the length of a short book like my Gödel Without Tears. Books in the series are aimed at providing “a dynamic reference resource for graduate students [and] researchers”. And that’s already a tall order for a book on this topic, at any rate: for most graduate students in philosophy (even if logic-minded) are likely to be pretty much beginners when it comes to tackling some set theory — and a book accessible to such beginners isn’t likely to also to be of much interest to researchers.

OK, forget the impossible prospectus, and let me try to assess the book in its own terms. First, I certainly enjoyed a quick read. It is engagingly written. And at various points in the later pages Burgess very helpfully put some order into my fragmentary knowledge, or offered genuinely illuminating remarks. So I endorse Rowsety Moid’s comment below, when he writes “I especially liked the second half — on ‘higher set theory’ — and the picture it gives of the various subject areas (descriptive set theory, continuum questions, combinatorial set theory) and techniques (large cardinals, forcing, inner models, infinite games, …) and of how they’re interrelated. I can’t recall anything else that gives as good an overview so briefly.” However, although set theory isn’t my special thing, I didn’t exactly come to this innocent of prior knowledge. And I do have to doubt whether later pages of the book will really be accessible to many of the intended student audience. OK, if may be that all the materials have officially been given to understand e.g. the Levy Reflection Principle on p. 55: but I suspect that a significant amount of mathematical maturity, as they say, would be needed to really appreciate what’s going on.

In headline terms, then, I don’t think that the book as a whole would work as advertised for many students. Still, the first half does make a nice motivating introduction, but one to be followed by (or as RM again comments, perhaps better read in conjunction with) a standard accessible introduction to set theory like Goldrei or Enderton. And then the enthusiast can return to try reading from §8 “Topics in Higher Set Theory” onwards to get a first overview of a few further more advanced topics, with a hope of getting a first inkling of what some of the interesting issues might be, before tackling a second-level set theory text.

Updated to use a comment from RM!

The Logic of Number

Having been so very struck by Russell and Frege as a student —  a long time ago in a galaxy far, far away — I have always wanted some form of logicism to be true. And the deviant form canvassed by Tennant back in his rich 1987 book Anti-Realism and Logic (I mean, deviating from neo-Fregean version we all know) is surely worth more attention than it has widely received. So I’m looking forward to reading Tennant’s latest defence of his form of logicism, in his new book The Logic of Number, published a few weeks ago at a typically extortionate OUP price.

On a quick browse, the book goes in a somewhat different direction to what I was expecting, having read Tennant’s 2008 piece ‘Natural Logicism via the Logic of Orderly Pairing’. The additional new apparatus for developing arithmetic added in that paper seems not to be in play again here. Rather, the book doesn’t (I think) develop arithmetic as far, but instead goes on to discuss logicist accounts of rationals and reals.

I’ll perhaps try to say something more about the book in due course, when some other reading commitments are done and dusted. Meanwhile you might well in fact be able to take a look if interested. For The Logic of Number, I’m glad to say, has just been also made available at Oxford Scholarship Online. So if your university library has a suitable OUP subscription, it should be free to read.

An Introduction to Proof Theory, Ch. 7 and Ch. 9

The overall strategy of Gentzen’s consistency proof for PA can be readily described. We map proofs in his sequent calculus version of PA to ordinals less than 𝜀0. We show that there’s an effective reduction procedure which takes any proof in the system which ends with absurdity/the empty sequent and outputs another proof with the same conclusion but a smaller assigned ordinal. So if there is one proof of absurdity in PA, there is an infinite chain of such proofs indexed by an infinite descending chain of ordinals. That’s impossible, so we are done.

The devil is in all the details. And these will depend, of course, on the exact system of PA which we work with. If we do indeed start from something close to Gentzen’s own system, then things quickly get obscurely intricate in a very untransparent way. The assignment of ordinals initially seems pretty ad hoc and the reduction procedure horribly messy. It is the presence of PA’s induction rule which causes much of the trouble. So as Michael Rathjen suggests in his entry on Proof Theory in the Stanford Encyclopedia, it turns out to be notably more elegant to introduce an infinitary version of PA with the omega-rule replacing the induction rule, and then proceed in two stages. First show that we can unfold any PA deduction into a PA𝜔 deduction, and then do a significantly neater Gentzen-style consistency proof for PA𝜔 (the general idea was worked out by Schütte, and is familiar to old hands from the tantalizing fourteen-page Appendix in the first edition of Mendelson’s classic book!).

Mancosu, Galvan and Zach, however, stay old-school, giving us something close to Gentzen’s own proof. Even with various tweaks to smooth over some bumps, after an initial dozen pages saying a bit more about PA, this takes them sixty-five pages. And yes, these pages are spent relentlessly working though all the details for the specific chosen version of PA, with extended illustrations of various reduction steps. It is not that the discussion is padded out by e.g. a philosophical discussion about the warrant for accepting the required amount of ordinal induction; nor are there discussions of variant Gentzen-style proofs like Schütte‘s. Is the resulting hard slog worth it?

A mixed verdict (and I’ll be brief too, despite the length of these chapters — as I don’t think there is much profit in trying to summarise here e.g. the stages of the reduction procedure, or in looking at particular points of exposition). There’s something positive to say in a moment. But first the more critical comment.

It sounds so very very ungrateful, I know, but I didn’t find the level of exposition here that brilliant. The signposting along the way could be more brightly lit (long sections aren’t subdivided, and [mixing my metaphors!] crucial paragraphs can appear without fanfare — see e.g. half way down p. 280). And more importantly, page by page, the exposition could often be at least a couple of degrees more perspicuous. It is not that the proof details here are particularly difficult; but still, and really rather too often, I found myself having to re-read or backtrack, or having to work out the motivation for a technical detail for myself. I predict, then, that many of IPT’s intended readers (who may, recall, “have only a minimal background in mathematics and logic”) will find this less than maximally clear, and — to say the least — markedly tougher going than the authors wanted. The logically naive reader will struggle, surely.

But now forget about  IPT’s official mission-statement! On the bright side, the more sophisticated reader — someone with enough mathematical nous to read these chapters pausing over the key ideas and explanations while initially skipping/skimming over much of the detail (and having a feel for which is likely to be which!) — should actually end up with a very good understanding of the general structure of Gentzen’s proof and what it is going to take to elaborate it. Such a reader should find that — judiciously approached — IPT provides a more attractive introduction than e.g. Takeuti’s classic text. So that’s terrific! But as I say, I think this probably requires a reader not to do the hard end-to-end slog, but to be mathematically able and confident enough to first skim through to get the headline ideas, and then do a second pass to get more feel for the shape of some of the details; the reader can then drill down further to work through as much of the remaining nitty-gritty that they then feel that they really want/need (though for many, that is probably not much!). For this more sophisticated reader, prepared to mine IPT for what they need in an intelligent way, these chapters on Gentzen’s consistency proof will indeed be a great resource.

And on that happier note, let me end!

An Introduction to Proof Theory, Ch. 8

As I said in the last post, Chapter 7 of IPT makes a start on Gentzen’s (third, sequent calculus) proof of the consistency of arithmetic. Chapter 8 fills in enough of the needed background on ordinal induction. Then Chapter 9 completes the consistency proof. I’ll take things in a different order, commenting briefly on the relatively short ordinals chapter in this post, and then tackling the whole consistency proof (covering some 77 pages!) in the next one.

§8.1 introduces well-orders and induction along well-orderings, and §8.2 introduces lexicographical and related well-orderings. Then §§8.3 to 8.5 are a detailed account of ordinal notations for ordinals less than 𝜀0, and carefully explain how these can be well-ordered.

Mancosu, Galvan and Zach rightly make it very clear that we can get this far without taking on board any serious set theoretic commitments. In particular, the ordinal notations are finite syntactic objects and, if o1 and o2 are two distinct notations, it is decidable by a simple procedure which comes first in the well-ordering. However, §8.6 does pause to present “Set-theoretic definitions of the ordinals”, and the discussion continues in §8.7 and §8.8. These are written as if for someone who knows almost no set theory: but I suspect that they’d go too fast for a reader who hasn’t previously encountered von Neumann’s implementation of the ordinals by sets. (And I’d certainly want to resist our present authors uncritical identification of ordinals with their von Neumann implementations! — ordinals are numbers that can be modelled in set theory in the way that other kinds of numbers can be modelled in set theory, but are not themselves sets. But that’s a battle for another day!)

The chapter finishes with §8.9, where sets drop out of the picture again. We here get a brisk treatment of arguments by ordinal induction up to 𝜀0 for the termination of (i) the fight with the Hydra, and (ii) the Goodstein sequence starting from any number. These are lovely familiar examples: the discussion here is OK, but not especially neatly or excitingly done.

Back though to the earlier parts of the chapter, up to and including §8.5. These are pretty clear (though I suppose parts might go a bit quickly for some students). They should do the needed job of giving the reader enough grip on the idea of ordinal induction to be able to understand its use in Gentzen’s consistency proof. Onwards, then, to the main event …!

To be continued

An Introduction to Proof Theory: where next?

Let’s pause to take stock. Chapters 3 to 6 of IPT comprise some two hundred pages — a book’s worth in itself — on Gentzen-style natural deduction and normalization theorems, and then on the sequent calculus and cut-elimination theorems. These topics are much-discussed elsewhere, at various levels of sophistication. What’s distinctive about the coverage of IPT is that it is (i) supposed to be accessible to near beginners in logic, while (ii) sticking pretty closely to discussing Gentzen’s own formal systems, and Gentzen’s own proofs about them (and later developments of them): “One of the main goals we set for ourselves,” say the authors, “is that of providing an introduction to proof theory which might serve as a companion to reading the original articles by Gerhard Gentzen.” Moreover, (iii) “In order to make the content accessible to readers without much mathematical background, we carry out the details of proofs in much more detail than is usually done.”

In discussing these four chapters, I’ve quibbled about various points of presentation. But I suppose my main unhappiness has been about the overall shape of the project itself, given the intended readership. Gentzen is often a remarkably clear writer; but I’m not at all convinced that sticking so closely to his original papers is the best way to start learning about structural proof theory. And I’m even less convinced that giving massively detailed proofs is the way to help the beginner get clear about the Big Ideas (especially when so many of the details are pretty tedious, and are made more tedious by the decision to cleave to Gentzen’s original formal systems). Of course, I’m not the intended naive reader, and (unlike the authors!) I haven’t given lecture courses on proof theory: maybe their approach works a treat with many students. All I can do is register my doubts, and (as I have done in passing) suggest familiar alternatives that on balance I would recommend more warmly to beginners, who can then dip into IPT if/when they feel the need.

But now we move on to the last three chapters of the book. These focus on Gentzen’s third proof of the consistency of arithmetic — the one using ordinal induction  in the setting of a sequent calculus presentation of arithmetic. Chapter 7 makes a start at setting up the proof. Chapter 8 pauses to explain ordinal notations and the idea of ordinal induction. Then the final Chapter 9 makes use of ordinal induction to complete the consistency proof.

Now, while there are quite a few other options for expositions of natural deduction and sequent calculi available for readers with different levels of mathematical sophistication but little background logic, here the situation is surely quite different. Yes, there are a fair number of very short presentations (a few paragraphs) giving an arm-waving explanation of the basic proof-idea of Gentzen’s second or third proofs: but we don’t have even an handful of worked through but still accessible accounts of how the argument goes. There’s the chapter in Gaisi Takeuti’s justly admired 1975 Proof Theory, but that’s fairly tough going for anyone. I’ve seen the long Chapter 1 of Wolfram Pohler’s 1989 Proof Theory described as giving “a very clean, streamlined approach”, but — to say the very least — it will be impenetrable for the relative beginner. There’s a little 77 page 2014 book by Anna Horská with the promising title Where is the Gödel-Point Hiding: Gentzen’s Consistency Proof of 1936 and his Representation of Constructive Ordinals. It’s dreadful. What else is there?

Paolo Mancosu, Sergio Galvan and Richard Zach therefore have little competition here. Any decent presentation of Gentzen’s argument which makes it more available will be very welcome. And, taking a very superficial look at the next chapter, it seems that you don’t have to have read all the previous chapters in order to join the party here. Assuming you already know a bit about the sequent calculus and cut elimination proofs, my impression is that a quick skim of Chapter 6 will be enough to set you up for diving into Chapter 7. Which is good.

These final chapters are the ones that I’ve been most looking forward to seeing: so how do they work out?

To be continued

Scroll to Top