2015

I’m trying to think about how OLT would work if read, as is, by a student as a stand-alone text, as an introduction to its topics. That is, of course, a quite different issue from e.g. the question of how useful it will be to teachers to take and adapt chunks of the text and weave them into their own notes backing up a lecture course!  So read the continuing comments in that light:

Part III: Computability (pp. 105-158) Ch. 9 is on Recursive Functions, and is reasonably clear but brisk (I think that non-mathematicians encountering this material for the first time will not find it easy and will need to read around in more discursive texts). Ch. 10 gives us 11 pages on the Lambda Calculus: this is surely either too much or too little. Almost nothing later depends on this, so the chapter can certainly be skipped. On the other hand, those baffled by the Lambda Calculus (in my experience, quite a few when they first encounter it, even among good maths students) will find this too quick to be terrifically helpful. An opportunity missed, perhaps.

Ch. 11 is rather different. This is a twenty-five page overview of Computability Theory getting as far as Rice’s Theorem: this is decently well done. Again I’m not sure there is enough detail for a first pass through this material: but I could recommend it as making useful revision material.

Part IV: Turing Machines (pp. 160-167). Chs. 12 and 13 are very short, and evidently awaiting considerable expansion.

Part V: Incompleteness (pp. 169-205). I have a horse in this race, of course, so am interesting to see how others canter down the track! Ch. 14 is on the Arithmetization of Syntax. It is difficult to do this stuff with a light touch, and (as elsewhere in OLT) I’d go for adding quite a lot more arm-waving motivation, here along the lines of “Look, consider the relation Pr(p, n) which holds when p codes for a well-formed proof in Q of the wff with number n.  It’s easy to see that you can check whether Pr(p, n) without going in for any open-ended searches; here, informally, is how. So Pr is going to be primitive recursive, right?”. And since the chapter takes PA to be formalized in a sequent calculus, the details of arithmetization are inevitably a bit messy.

Ch. 15 is on Representability in Q. This is done the standard way, via the $latex \beta$-function lemma, and we get out the undecidability of Q and hence of FOL. Then Ch. 16, Theories and Computability,  shows that consistent extensions of Q are undecidable, and complete computably axiomatised theories are decidable — which together give us, in a familiar way, that consistent, computably axiomatized extensions of Q are incomplete. (Oddly, the undecidability of FOL is again proved along the way, without comment.) Ch. 17 then gives a more Gödelian proof of incompleteness via the fixed point lemma: it would perhaps have been good to say more about how this relates to the preceding proof. And then we have something pretty brisk on the Second Theorem and Löb’s Theorem. These chapters are reasonably clear. Stylistically, however, we are looking more at spruced-up (or not so spruced-up) notes rather than a discursive text:  so they are not — I would have thought — as accessible or helpful to the beginner as a number of excellent treatments in the well-known literature.

Part VI: Sets, relations, functions (pp. 207-229). This is really an Appendix, the ‘little bit of set theory you need to know’, done at a very introductory level, getting as far as telling us about Cantor and non-enumerable sets. These pages are routine but clear enough. Naughtily, they tell us that functions are relations (Great Uncle Gottlob sighs, but he is used to this). Oddly, they introduce ordered pairs without tellings us how to represent them by sets, so there is something missing here. But this part is on its way to being a handy stand-alone module.

A general reflection on OLT. Having got to the end, it is clear that the different segments by different hands presuppose quite significantly different levels of sophistication from the reader. This makes me wonder a bit about the wisdom of presenting this resource as one long document rather than as a suite of separate modules. From the point of view of the rather daunted student, splitting things up would make it a lot clearer that you can and should  pick and choose various parts, depending on your background and interests. But also dividing things into modules might encourage the potential contributor.

Logic teachers are a very picky lot with a tendency to think that other people’s books usually Do It Wrong (which is why we too often try to write our own)! So faced with one big text, most will find aspects to be pretty unhappy about, muttering “this just isn’t the best approach to getting this material across”. Suppose you think OLT is going about things the wrong way in Parts X and Z: then, at least speaking for myself, if you are therefore not really wedded to the overall book, you aren’t going to be very inclined to chip in to help improve Part Y (even if that is a part you rather like). So I wonder whether it would sell the project more strongly, be more enticing to students, and also encourage more potential contributors to various segments, if OLT were carved into quite separate modules?

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.

If you have read the Teach Yourself Logic 2015 Study Guide, then you will know that I there particularly recommend as an admirably lucid and, yes, friendly introduction to first-order logic Christopher Leary’s 2000 book, A Friendly Introduction to Mathematical Logic. Very regrettably, Prentice-Hall let this excellent book go out of print (though that was no reason not to continue recommending it in the Guide, which is largely aimed at students likely to have access to a library). But that cloud has turned out to have a silver lining. The copyright having reverted to the author, he has got together with Lars Kristiansen to produce a much expanded second edition, with seventy pages more text (on computability) and over seventy pages of solutions to exercises. A copy has just landed on my desk, and it is all looking very good. Moreover, this second edition has been published through Leary’s university library. I ordered my copy via Amazon, and evidently it is printed (on demand?) by Amazon, and very inexpensively too. So this bigger and better second edition will be notably more affordable by students.

I’ll no doubt say more about this new edition in the updated 2016 version of the Guide. In the meantime, make sure your university library gets a copy or two! (ISBN-10: 1942341075)

Tony Roy has kindly alerted me to the existence of his freely available Symbolic Logic: An Accessible Introduction to Serious Mathematical Logic.

It is now in version 7.1, so I guess I should have discovered this before! It looks, at a quick first glance, a remarkable resource; still work in progress but looking very polished. There are no less than 746 pages together with another almost 200 pages of answers to exercises. It goes from an introduction to sentential logic, through the usual topics in first order logic (presented both axiomatically and in a natural deduction system) getting as far as e.g. a discussion of compactness and the downward L-S theorem, and then moving on to some quite detailed work on Gödel’s incompleteness theorems. And Tony writes that “it’s aimed especially at accessibility and so builds in a level of explanation and detail that may be missing from other sources.” So I’ll certainly be taking a look at this for TYL2016, and probably commenting there. In the meantime you can take a look yourself on the book’s website here.