Peter Smith's Blog, page 98

Teach Yourself Logic — suggestions? [Repost]

[I posted this back in August: and I’m moving this to the front of the blog to invite more contributions/suggestions!]

I haven’t looked at all at the Teach Yourself Logic Study Guide since the 2015 version came out on January 1st. I earlier had it in mind to do a mid-year update in time for the new (northern hemisphere) academic year: but that bird has long flown. The main Guide continues to be downloaded eighty or more times a month. It certainly seems to serve some need, and I get appreciative emails.  So I will put time aside over the coming months to get a 2016 version ready for next January 1st.

So now’s the time for feedback on both style and content. As far as style goes, while keeping to the spirit of the present Guide, what would make it more user-friendly? Should I keep the one-big-PDF format, or go over to a suite of webpages? [Added: after thinking a bit, I continue to incline strongly to the PDF format — it is easier to maintain, but also easier to read off line, and for students to work with by highlighting, commenting, etc. onscreen. But thoughts on style/layout etc. are still very welcome.]

As to content, any suggestions for additions, improvements? One thing I’ll want to say something about is The Open Logic project [added: I’ve posted some thoughts that  recently] But are there more conventional new(ish) publications, or overlooked older publications,  that could definitely rate a recommendation for student use?

Feedback from logicians at any stage of their career, whether taking first steps or on their zimmer frame, will be most welcome — either in the comments below, or by email (address at the bottom of my “about” page here).

And now for something completely different ….

And it is just Week 3 …

Moving gently on …

Autumn sun, Cambridge on the first day of lectures

I’m planning to go to a couple of lecture courses this term (including Peter Johnstone’s famed, take-no-prisoners, category theory course), and probably will join in a weekly reading group too. I also need to do quite a bit of other reading over the coming weeks if I’m to put together a decent update for the Teach Yourself Logic guide for 2016. Hence work on revising the category theory notes — already going at, shall we say, a rather gentle pace — will no doubt slow even more. So I thought I would put online the current version of Category Theory: A Gentle Introduction even though it doesn’t reach a natural break point. So far then, the now fourteen chapters (123 pp.), after introducing categories, consider limits and exponentials (constructions within categories) before moving on to start talking about functors (maps between categories). The category theory page here indicates which chapters to then read in the old notes, if you are feeling suitably enthused!

The Aïda of our dreams?

Aïda is perhaps one of those operas where the performance of our dreams is likely to beat any staging: we turn up the headphones, and our imagination does the rest.

The much heralded new studio recording of Aida, conducted by Antonio Pappano and with a stella cast, has now been released. You can listen, e.g., on Apple Music (surely worth a month’s subscription by itself!). I’m not sure this will supersede e.g. the legendary Karajan/Tebaldi/Bergonzi recording in my affections. But oh, it is pretty wonderful. Just listen to Jonas Kaufmann singing Celeste Aïda, and you’ll be hooked …

Git, for the rest of us?

Git is a widely used version control system, much used e.g. by software developers. But others, even writers of one-author paper or book projects,  swear  by it too. Thus Richard Baron writes:

The last time the Open Logic Text was discussed on the Logic Matters blog ( http://www.logicmatters.net/2015/05/10/the-open-logic-text/ ), there was some discussion of the merits of Git, and Richard Zach put up some material on the OLT blog about the use of Git. Since then I have experimented on GitLab, starting from zero knowledge, and can confirm that it is a wonderful system, even for a one-author project. So I encourage everyone to have a go.

This is from the comment thread here, where a discussion continues. This post is simply to point out the exchange to anyone interested in this sort of thing (but who might not be delving into comments on OLT). And to invite anyone else who has views/experiences about Git or some other version control system (as a paper/book author) to share them —  either in that thread, or [better?] in new comments here.

Book Note: The Open Logic Text, #2

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 rather 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 -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 (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?

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.

A Friendly Introduction to Mathematical Logic

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)

The art of not reading

Wise words, found in my twitter stream:

The art of not reading is a very important one. It consists in not taking an interest in whatever may be engaging the attention of the general public at any particular time. When some political or ecclesiastical pamphlet, or novel, or poem is making a great commotion, you should remember that he who writes for fools always finds a large public. – A precondition for reading good books is not reading bad ones: for life is short.

That’s from Arthur Schopenhauer, Essays and Aphorisms. Obviously, he was really  thinking of blogs and websites. And twitter streams.

This too:

Buying books would be a good thing if one could also buy the time to read them in: but as a rule the purchase of books is mistaken for the appropriation of their contents.

PHQ in astonishing form, again

PHQ at the Gramophone Awards ceremony

To the Wigmore Hall this morning, to hear the Pavel Haas Quartet play Schubert’s “Rosamunde” Quartet and Beethoven’s “Serioso”. An extraordinary short concert, with the PHQ at their unsurpassed best.

Of recorded performances of the “Rosamunde”, I perhaps know the Lindsays’ the best. This morning, the PHQ’s opening was as yearning, as emotionally charged; but the playing was tauter than the Lindsays’, the dynamic contrasts more marked, with the long first movement always unfolding with such a sense of the structure. I found it very moving indeed.

The opening of the second movement begins with the first violin playing the theme borrowed from Rosamunde. If you look at the score (oh the joys of the internet!), you might be surprised, as I was afterwards, to find that the opening bar, dah-de-de dah dah, is actually written as staccato  notes, albeit slurred staccato notes.  But  Peter Cropper, for the Lindsays, takes the slurring to the point that there is hardly any staccato to be discerned. And this is the way we usually hear the phrase played (compare, for just one example, Corina Belcea in another fine recording). Veronika Jarůšková, however, clearly marked the staccato notes. A few others do, like in the Emerson’s recording: but oddly in their hands the result is strangely flat, while Jarůšková made the phrase dance. And as the phrase returned and returned, initial surprise became very happy acceptance.

The last two movements of the Rosamunde were equally impressive. Compared again with the Lindsays, for example, the PHQ play with even more passion, more dynamics (the fs are indeed unmistakably forte, the pps musical whispers). When called on, Peter Jarusek’s cello drives the music forward almost fiercely, giving an usually weighty texture to the quartet — but this is all intensely controlled in a way that gives their music-making such emotional power. Astonishing. This was indeed Schubert to compare the PHQ’s hugely admired, award-winning, recording of  Schubert’s “Death and the Maiden” and the Quintet.

We would have gone home happy at this point. But if anything, the performance of the Beethoven quartet was even better. PHQ have been playing the “Serioso” occasionally for a long time, and there is even a CD recorded in 2008 for the BBC. That recording was really pretty good, but this morning’s performance was in a different league and has me reaching for the superlatives again. Making real sense of this compressed music, responding to its dramatic complexities, intense but never losing the extraordinarily tight ensemble, this was quartet playing at its finest.

We weren’t the only ones who thought that. The mostly grey-haired audience at the Wigmore are (to be frank) not a very spritely lot, so not inclined to spring lithely to its feet in a standing ovation. What we offer instead is a sitting ovation, with hands clapping above our heads. This morning, the four smiling players returned to the stage to acknowledge a sea of arms raised in loud admiration, and even a chorus of “bravo”s. Richly deserved it was, too.