Book Note: The Open Logic Text, #1

It has been nine months since I really looked at the Teach Yourself Logic 2015 Study Guide. It’s time to start thinking about a 2016 update. So over the coming weeks I’ll be tinkering with the current version, while reading, dipping, skimming and skipping though various logic books old and new  (I have far too long a list!). I’ll be posting here some Book Notes on individual texts as I go along. So here’s the first instalment on the first book, the new Open Logic Text.

This is a collaborative, open-source, text book, and very much work in progress. The book’s website describes the project like this:

The Open Logic Text is an open-source, collaborative textbook of formal (meta)logic and formal methods, starting at an intermediate level (i.e., after an introductory formal logic course). It is aimed at a non-mathematical audience (in particular, students of philosophy and computer science), but is completely rigorous.

The project team is distinguished: Aldo Antonelli, Andy Arana, Jeremy Avigad, Gillian Russell, Nicole Wyatt, Audrey Yap, and Richard Zach. You can get a current version of the complete text (pp. 229) and also a sample course text Intermediate Logic selected and remixed from OLT (pp. 138) from this download page.

I don’t have any settled view on the likely merits or otherwise of this sort of collaborative project, but of course wish it well, and will be very interested to see how things develop. My comments here are on the complete text as retrieved on 2 Oct. 2015.

Part I: First Order Logic (pp. 9-64) What do these opening chapters cover? Ch. 1 is on the syntax and semantics of first-order languages. Ch. 2 talks about theories and their models. Ch. 3 presents the LK sequent calculus and proves its soundness. Ch. 4 proves the completeness theorem by Henkin’s method (and touches on compactness and the downward LS theorem).

That’s a packed program for less than sixty pages. And a non-mathematical student who tackles it will have to bring more to the party than she is likely to have picked up from a typical introductory formal logic course. Five pages in, it is assumed that the reader knows what an induction hypothesis is and how proofs by induction work. A couple of pages later, we are told that a certain definition is a ‘recursive’ definition of a function, again without explanation. When it comes to talking about first-order theories, we get as first examples the theory of strict linear orders and the theory of groups, with no explanation of what such things are. A bit later, Cantor’s theorem is mentioned as if already familiar (in remarking that the formal language of first-order set-theory suffices to express it). And so it goes. Actually, a mathematically rather ept audience seems to be presupposed!

As noted, the proof system considered is the sequent calculus LK. There isn’t a word to link this up to what a student may have encountered in her introductory formal course (very likely a tree-based system, or a Fitch-style proof system), or to explain why we are doing things this way. We get a few examples, and then a three-page soundness proof. Again, tough for the non-mathematical, I’d have thought. So far, in fact, this all reads like slightly souped up lecture hand-outs covering some of the fiddly bits of a course, very respectable if accompanied by a lot of lecture-room chat around and about, but not amounting yet to a stand-alone text book.

Having adjusted to the level of the enterprise, however, the chapter on completeness is pretty clearly done, with the strategy of a Henkin proof (and the pitfalls that have to be negotiated to get the proof-idea to fly) being well explained. This could make useful revision material for students doing courses based on other books as it isn’t tied to LK.

Part I, continued: Beyond First Order Logic (pp. 65-79) After a short overview, the sections of Ch. 5 are titled ‘Many-sorted logic’, ‘Second-order logic’, ‘Higher-order logic’, ‘Intuitionistic logic’, ‘Modal logics’, ‘Other logics’. Yes, in just fifteen pages. The pages on second-order logic are probably useful, enough to give a student a flavour of the issues. Otherwise, the discussions are necessarily pretty perfunctory — place-holders for later developments.

Part II: Model Theory (pp. 81-103) The website tells us that these twenty-four pages come from Aldo Antonelli’s notes. The assumed sophistication of the reader goes up another notch or two. These are pretty terse maths notes in the conventional style (and none the worse for that! — but perhaps again not quite fitting the advertised brief).

Ch. 6 comprises just ten pages on ‘The Basics of Model Theory’ (including the usual proof that countable dense linear orderings without end points are isomorphic, and a brisk discussion of non-standard models of first-order True Arithmetic). Then Ch . 7 proves the interpolation theorem and derives the Beth definability theorem. Ch. 8 proves Lindström’s theorem.

Now I would not have counted full proofs of interpolation and  Lindström’s theorem as entry-level topics on model theory. And that’s not me being idiosyncratic. Cross-checking, I find  that Manzano’s nice elementary text on model theory doesn’t get to either. Even the bible, Hodges’s Shorter Model Theory, never gets to Lindström’s theorem — and we don’t meet interpolation until half way into that book.

So I wouldn’t yet advise tackling these pages as initial reading on model theory. However, taken as standalone treatments for those with enough background, Chs. 7 and 8 are actually crisply and clearly done, and so could well be recommended e.g. as supplements to Manzano or other introductions.

To be continued.