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 ( ), 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.

Posted in This and that | 20 Comments

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 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(pn) 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 \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?

Posted in Books, Logic | 6 Comments

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.

Posted in Books, Logic | 14 Comments

A Friendly Introduction to Mathematical Logic

41fXkfrMC0LIf 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)

Posted in Books, Logic | 2 Comments

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.

Posted in This and that | 1 Comment

PHQ in astonishing form, again

PHQ at the Gramophone Awards ceremony

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.

Posted in Music, Pavel Haas Qt | Leave a comment

A Gentle Introduction

You can now download here the first instalment (88pp.) of a Gentle Introduction to category theory, reworked from my Notes on Category Theory.

Gentleness is relative, of course. Peter Johnstone plans, in his first 13 lectures for this (academic) year’s Part III course, to get through rather more that I’ll be covering in 250+ pages: so compared with that relentless, take-no-prisoners, pace, I’m taking things very gently indeed. Some might well think too gently: I can only say that in my experience taking the beginnings of category theory slowly, firmly nailing down the basics, really pays off when it comes to tackling more advanced stuff.

On the other hand, some logic-minded philosophers without much mathematical background, but having heard that category theory is supposed to be illuminating about structuralism and foundational matters, will probably still find my Gentle Introduction pretty tough. All I can say to them is that I’ve tried to make things a lot more accessible than some of the alternative available routes into category theory.

One major change from the previous Notes, which followed roughly the order of the syllabus of the Part III course last year, is that I will be tackling topics in a different order (different too from that given in Peter Johnstone’s outline for this year). The plan is to look first at what happens inside categories (limits, exponentials, etc.) before looking at maps between categories (functors) before looking at relationships between maps-between-categories (natural transformations, eventually adjunctions). McLarty in the first two parts of his much faster-paced Elementary Categories, Elementary Toposes, did things this way, and it surely has a certain logical appeal.

I toyed with the idea of releasing small segments of the Gentle Introduction week-by-week, alongside some exercises to go along with the segments. But I then thought better of it. It’s just too unpredictable when writing will zoom ahead, when it will hit blocks. So I’ll just release updates of the Gentle Introduction when they are ready (check the categories page here for the date of the latest version, and for an indication of which remaining chapters from the old Notes you might want to go on to read.) Maybe I’ll run an online “course” with exercises some time in the new (calendar) year when I’ve got a full set of updated notes in the bag.

Posted in Category theory | Leave a comment


There was an article in the Guardian a few days ago on Why does music give us chills? (shivers down the spine, goosebumps…). This has been the subject of  some interesting neuropsychological investigations; there are a few links in the article. I was surprised to learn that such chills are only experienced by about half the population — and even more surprised (to put it mildly) by what some of those interviewed at the end of the article reported as giving them the sensations. Still, here for your delight, I hope, is something that works for me. I wasn’t quite sure what performance to link to: dramatically, perhaps this is better. But while it may be a little hard to believe in Anna Netrebko here as a Gilda (such is her undimmable megawattage as a diva), she and Elina Garanca, Ramon Vargas and Ludovic Tézier, certainly deliver the chills:

Posted in Music | Leave a comment

Tony Roy: Symbolic Logic

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.

Posted in Books, Logic | Leave a comment

One future for journal publishing

On his blog, Tim Gowers has announced a new journal, Discrete Analysis for which he is to be the managing editor. The content of the journal probably won’t be of much interest to most readers of Logic Matters. It will cover topics in additive combinatorics and other topics which have a suitable family relationship. But the form of the journal is fascinating, and will surely come to be emulated by other editorial groups for other areas of mathematics. It is to be an arXiv overlay journal. What this means, in Tim Gowers’s words, is that

rather than publishing, or even electronically hosting, papers, it will consist of a list of links to arXiv preprints. Other than that, the journal will be entirely conventional: authors will submit links to arXiv preprints, and then the editors of the journal will find referees, using their quick opinions and more detailed reports in the usual way in order to decide which papers will be accepted. … [So] The articles will be peer-reviewed in the traditional way. There will also be a numbering system for the articles, so that when they are cited, they look like journal articles rather than “mere” arXiv preprints. They will be exclusive to Discrete Analysis.

There’s much more in the very lucid and persuasive blog post, about both principles and practicalities.  Plainly this is one way forward for journal publishing, one way to push back against the stranglehold of commercial publishers extorting funds from hard-pressed university libraries.

One issue I noted. Tim Gowers  only expects Discrete Analysis to get in the order of 50 submissions per year (less to start with). So — after the kerfuffle of setting up the systems and working through teething problems — this promises to be a relatively small commitment for the editorial board to keep running. However, the arrangements won’t so easily scale up: there is nothing in the funding model, as I understand it, to pay a managing editor of a bigger project an honorarium for a more substantial time commitment. But maybe keeping things small is no bad thing. I’m all for well-focused, relatively niche, journals. A more distributed network of small-ish arXiv overlay journals could well be the way to go (so long as, like Discrete Analysis, they don’t aim to set stern boundaries, so that interesting papers that break new ground sitting between familiar clusters of topics can still find a home).

I wonder if any logicians out there are thinking of starting such a journal?

Posted in This and that | 2 Comments