Well, that proved popular

Back in December, I posted what I thought might be an enticing offer to advertise new logic books at the top of the right-hand column, given the relatively high traffic of logic-minded visitors here. For the last four months, then, there has been a thumbnail of my own Gödel book there, with the caption ‘Publicize your new book here’, linked to that now-deleted post explaining the proposed (very modest) deal.  I’ve had exactly one expression of interest (for a book some way off appearing). I guess the offer wasn’t so very enticing after all.

One thing I’ve learnt over the blogging years is that it really is pretty unpredictable what does and what doesn’t generate any interest!

Posted in This and that | Leave a comment

Gödel Without Tears, for onscreen reading

Just to say that my Gödel Without Tears notes can now be downloaded in two versions, differing only in formatting. There’s the A4 version as before: but also a version reformatted to suit the screen proportions of an iPad which will be better for onscreen reading on such devices (or perhaps on a divided a laptop screen).

Posted in Gödel's theorems | Leave a comment

Your blogger in his study, waiting for light to dawn


OK, that’s really Augustine of Hippo as portrayed by Carpaccio in his cycle of paintings for the Scuola di San Giorgio degli Schiavoni in Venice. But, forgetting the mitre and crozier,  it’s much the same clutter here …

Posted in This and that | Leave a comment

Tableaux or not tableaux, #3

The situation, perhaps we can nearly all agree, is this. In a first formal logic course for philosophers there’s a lot we’ll want/need to pack that’s independent of the nitty-gritty of a deductive apparatus of any particular formal proof system you might want to introduce. (I notice that in my  Introduction to Formal Logic elaborating my lecture course, no less than 27 of the 36 short chapters are on matters other than the actual tableaux system it uses — nearly 20 of those chapters are really on matters round and about the formal languages that would shared by different proof systems). Also, it behoves us to remember that a fair proportion of our class will find even these other parts of the logic course tough, before ever getting down to trying to manipulate our favoured proof system.

So, given the limited proportion of our time we can devote to developing a formal proof system (assuming we want to do that) and given the level of formal work we can sensibly hope to get our typical student to cope with, what to do? — assuming we aren’t just going to sail on without worrying about most of the class falling overboard at this point.

Gentzen-style deduction systems are — of course, as we all know — the Right and Proper Way of doing logic as nature intended! But by my lights, they aren’t so readily manageable by non-mathematical beginners. (Be honest: if you have to discover a rather tricky Gentzen-style proof, how do you do it? — I bet the answer, for a good number of us, is that you roughly sketch out something more Fitch-style, think “Aha, that’s the way a proof can go!”, and then massage the sketch into an official Gentzen-style tree!). So setting aside such systems for introductory purposes, and also setting aside axiomatic systems and sequent calculi (lovely though they are if our focus is on metalogical investigation), then I guess that really leaves us with Fitch-style calculi and tableaux systems. Which are indeed surely the usual options these days.

There are pros and cons on both sides, and it would be absurd to dismiss either option: indeed, it would be great to be able to look at both, but constraints of time will no doubt force a choice. (And constraints of space similarly forced a choice in my IFL where I really wanted another seven or eight short chapters on natural deduction, but CUP saw the matter differently!) As I said in the opening instalment of these posts, for a number of years, I did cast my vote for a Fitch-style natural deduction system. But I ended up teaching formal tableaux in the first year (leaving natural deduction to be covered briskly in a follow-up second-year course). Why so?

I think a major consideration was this. Tableaux for propositional logic give us mechanical procedures for demonstrating valid entailments to be so.  Moreover, when a tree stays open, we can read off a counter model demonstrating the invalidity of the argument being examined. The same goes for quantificational tableaux in simple cases; and it is only later on that you might have to use a bit of ingenuity to get a tree for a valid argument to close.

Stick to the propositional case for the moment: then the worst that go wrong for a careful student is that, by making injudicious choices of which rules to apply when, trees may sprawl more than is necessary. The student can do the logic without having to be smart at spotting proof strategies. Which is just great. For we all know that appreciating what it is to apply rules of a formally defined system (something we probably do want to get across) is one thing, and that having the ability to spot a proof strategy within that system is something else entirely — as is spectacularly illustrated in a Hilbert-style axiomatic system like Mendelson’s where it is very easy indeed to understand what constitutes a proof and can be ludicrously difficult to find a proof at least in the unaugmented system. Now, true enough, proofs in a Fitch-style system are a lot easier to find than in a Hilbert-style system: but even so, unless you mess about introducing redundant rules in inelegant ways, there will always be simple things that require somewhat tricksy proofs — and you will have to spend time drumming into your students’s heads paradigms for various cases they may encounter. And that, by my lights, is not a good use of your very limited time or of their logical efforts. If we suppose, not unreasonably, that with first year philosophers we should be more concerned to engender understanding of the principles of some formal system rather than giving a catalogue of tricks of proof-discovery, then starting with tableaux which they can at least (for quite a while) work without needing much ingenuity has its very considerable attractions. (Anecdotally, it was the most mathematically minded of the interested people on the faculty who were keenest on starting with tableaux for just these sorts of reasons.) Sure, when we get to some tableaux for arguments involving multiply-quantified propositions, the more mathematically ept students can get a chance to show off — but that comes later, as it should.

Of course we want our students to know what informal modus ponens, conditional proof, reductio, etc. are (and we’ll want to say something about how such moves can get chained together, e.g. when mathematicians build up proofs). But having a course which — when it comes to a formal system — uses tableaux doesn’t mean these things get lost (they can and should get covered in the large part of the course that isn’t specifically about your chosen formal system, and then we can return to formal natural deduction at a later stage). Of course we want our students to get clear about the difference between syntactic and semantic notions. But although there is a sense in which tableaux are semantically driven, we can reinforce the syntax/semantics distinction just as well in a tableaux-based course as in a course that focuses on natural deduction (see my book).

Having said all that, Fitch-style natural deduction is indeed lovely and, yes, natural. And if I had been teaching mathematics students who are already developing some informal notion of rigorous deduction then I’d have surely taught some form of ND (maybe indeed Gentzen-style) from the off, developing an interplay between their informal and formal understanding of rigorous proof. But it’s teaching beginning philosophers that we are talking about here, and that I think changes the calculation of pros and cons. I certainly understand the motivation for teaching a Fitch-style system to philosophers (as indeed my successor in teaching the first year Cambridge course has chosen to do). Yet I think, given my time over again, I’d still on balance go arboreal.

Posted in This and that | 3 Comments

Tableaux or not tableaux, #2

Exactly what you choose to put into a first formal logic course for philosophers, and the level of coverage you try to achieve, will be constrained by so many considerations which vary from university to university that there can’t possibly be a one-size-fits-all way of doing things. Have the kids already had an “informal logic/critical reasoning” module? How many lecturing hours have you got? Is there a system of frequent small-group tutorial classes backing up the lectures to go through exercises (and how much extra teaching can be done by TAs in that way)? Is this the only formal logic course offered in the first couple of years or is there a follow-up course in the second year (so it isn’t so much a question of what to teach as when to teach it)? What proportion of the class can be expected to have the equivalent of a top grade in A-level (high school) maths? What proportion are likely to be rather symbol-phobic humanities students? And so it goes …

I suppose, though, that we can agree — can we? — that part of what we’ll want to cover at some level in first course consists in topics such as these (put very roughly, so as not to prejudge too many choices on details of approach):

  • Basic ideas about deductive validity (and related notions like logical consistency and logical necessity) and the contrast between deductive and good-but-not-deductively valid inference. Ideas about the way deductively valid arguments can fall into patterns sharing the same form, etc.
  • The initial case of arguments relying on the connectives and/or/not; the ideas of a tautology and of tautological entailment; truth-table testing. You’ll want to connect this to important informal ideas like proof-by-cases, reductio-ad-absurdum, etc.
  • Relatedly, we need to explain a tidy formal language for regimenting this propositional logic, getting over the idea of strict syntactic formation rules, and the idea of interpretations/valuations for the language.
  • Along the way, we’ll have to say something about use and mention, quotation conventions and so on. And about the use of object-language variables vs schematic variables added to our English meta-language.
  • Now add informal reflections on varieties of conditionals, and considerations about which inferences are intuitively valid or otherwise for different kinds of conditional (e.g. when can we contrapose?). Also informal thoughts about ‘only if’ and ‘if and only if’. Then consider prospects for adding a workable conditional to our truth-functional language, expanding the truth-table test etc.
  • Now broadening our scope, we want to consider quantificational arguments. So we need to explain and motivate the usual sort of quantificational language QL (initially without identity and functions), again explaining the syntax very carefully and at least giving an informal understanding of the idea of an interpretation of the language (and hence of quantification validity as truth-preservation on any interpretations).
  • We want students to be confident in handling the language QL when they meet it in use elsewhere, so we are going to need to spend quite some time getting them happy with translation/transcription/regimentation (whatever you want to call in) from English into the formal language and back again.
  • Some informal discussion of examples of valid and invalid inferences of QL, and relation to vernacular arguments.
  • Now add identity. Discussion of what we can now translate using identity. Russell’s theory of descriptions. Ideally something about functions too.

I should add (prompted by David Makinson’s congenial comment below) that we’ll also want students early on to get a smidgin of knowledge about set notation and basic ideas, and perhaps a few ideas about probability too. If you have to wrap these topics too into the first “logic” course (in my case, I didn’t have to do that, as there were separate mini-courses on them), then things are getting even more crowded.

Now note that, as yet, we’ve said nothing about a formal deductive system, whether natural deduction (Fitch-style, Lemmon-flavoured, Gentzen style), tableaux, or — perish the thought! — axiomatic. Yet we have already got a pretty substantial menu to get through. And if you are going to cover it properly and in an interesting way, keeping the majority of your class on board, then the material I’ve mentioned so far is necessarily going to take up a goodly amount of time. In fact, I guess this part of the menu used to occupy two-thirds of my lecturing time in a 24 lecture course. So the question “what formal system to use” became for me “what can we usefully do in maybe seven or eight lectures”

Now, I was ridiculously fortunate in my last years of logic teaching. I was in Cambridge, where we can do our very best to pick the brightest/most promising students, and where we can demand (and get) very intense levels of term-time work, and set vacation work too. The students got a lot of first year logic lectures, with back-up examples classes taught by enthusiastic grad students. Even so, and despite the fact that I intentionally aimed the lectures at the non-mathematical majority, and we didn’t go out of our way to set nasty tripos questions at the end of the year, it was clear that quite a few even of these students find even the stuff I’ve mentioned (before we tackle a formal system) surprisingly tough. Lots of course sail through, but I learnt that, even in Cambridge, it is only too easy to under-estimate how foreign all this kind of thing is to many students, however smart they are. So the question in fact became “what can I usefully do in maybe seven or eight lectures, with students many of whom find thinking formally quite tough, without entirely losing too many people?”

To be continued.

Posted in This and that | 2 Comments

Tableaux or not tableaux, #1

The other day Sara Uckelman of Durham asked on Twitter about people’s favourite textbook for 1st year intro logic using natural deduction/Fitch-style proofs. And she piqued my interest by mentioning that Lemmon’s book was currently top of her list.

Now there’s a blast from the past! Forty-five years ago — oh heavens above — when very first starting out teaching logic, I used Lemmon’s Beginning Logic as our textbook. For back then, at least by today’s standards, there were relatively few choices for books with a reasonably modern flavour. Lemmon’s book indeed has considerable virtues, but ease of manipulation of his deduction system by the more symbol-phobic student turned out not to be one of them. One trouble is that his formal system isn’t, of course, really a natural deduction system but is a sequent calculus (with the sequents written in a slightly non-standard way, with the wffs on the left [of the unwritten sequent arrow] being labelled by numbers rather than written out in full). So as you go along though a proof, you have to keep an explicit tally of active assumptions at each step (unlike with a Fitch-style proof, where the layout does the work for you). And strategies for finding Lemmon-style proofs aren’t that transparent to many beginners. Indeed, in tricky cases, I’d find myself thinking though a Fitch-style proof, which indeed reflects natural deduction steps, and then making the result Lemmon-flavoured. So why not do things Fitch-style from the off?

Which is indeed what I eventually started doing when after a gap of a few years (having for a while swapped courses with a colleague), I started teaching intro logic again, making my own course handouts using a Fitch-style system.

I wasn’t being at all idiosyncratic, by the way, in finding Lemmon’s book unsatisfactory (in the sense of finding that, despite its other virtues, it was too unfriendly for rather too many students). Peter Millican wrote round to UK philosophy departments — maybe about 1980, before email was common —  to discover what books people used in their first-year logic courses; and the majority  reply was, if I recall right, “Lemmon, but …”. Lecturers, that is to say, used Lemmon, but with significant reservations about how well the book actually worked with their students. It’s not for nothing that quite a few of us, when computers came along to make the job so much easier, produced our own handouts, a number of which indeed grew up to become books.

I found that the students seemed to cope significantly better with the business of writing correct formal proofs in the Fitch-style setting, with less messy housekeeping to keep track of, and the very nice visual display of what depends on what. It’s not called a natural deduction system for nothing! Yet, for all that, at some point in the 80s, I did switch from starting with a Fitch-style system to starting with a tableaux system (as in Hodges’s book, or Jeffrey’s,  or later my own). And that’s what I continued to do for the thirteen years when I was the main lecturer for the formal part of the Cambridge first year logic paper. But why so?

To be continued

Posted in This and that | 6 Comments

Postcard from Venice


A wonderful eight days in Venice, staying a few yards from the delightful Campo San Giacomo dell’Orio.  As we remembered from our last visit (too long since), if you avoid Piazza San Marco, then even the most famous galleries, churches, etc., are very surprisingly quiet. When we visited the stunning Scuola di San Giorgio degli Schiavone, very high on the guidebooks’ lists of must-visit sights, there was just one other family there.

Much of our time though was spent, as it should be, simply wandering around quiet corners by foot and vaporetto. The weather was really kind. We ate (mostly) splendidly. We were bowled over again. Next time, we must stay for longer.

Posted in Italian matters | Leave a comment

La Traviata at La Fenice

Francesca Dotto singing Violetta was just stunning tonight. Here she is last year in Act I of La Traviata in the same fine production (filmed unofficially I suspect, but still well enough to give you some sense of both the staging and her performance).

Posted in Italian matters, Music | Leave a comment

Progress so gentle as to be hardly perceptible …

Work on the Gentle Intro to Category Theory has been going slowly for a couple of months. I’d got to the point where I needed to backtrack and think through what I wanted to say, in a couple of preliminary chapters, about sets and then about structures, before going on to talk about category theory as (inter alia) a framework for talking about  how structures-of-structures hang together.

The chapter on sets, in particular, has been causing me grief. This isn’t going to be one of those merely routine chapters about basic set theoretic notions and notations — I’m going to take it that anyone tackling even an intro on category theory is unlikely to need yet another run through those basics. Nor is this going to be a discussion of the fancy issues about big universes of sets that might or might not be needed for really big categories (after all, it’s only after we know quite a bit of category theory that it will become clear what the genuine issues are and how much of applicable category theory they affect).

No, what I want to write about are basic things that turn out to be relevant quite soon when we start talking about categories, like how much common-or-garden maths-talk seemingly about sets is really plural talk in thin disguise (and why plural talk should be taken at face value), and relatedly about how much set talk is about virtual classes in Quine’s sense. And then say something about what we get from having a more substantial set theory, and just how much substantial set theory is needed for ‘ordinary’ (non-set-theoretic)  maths, and why there is no unique theory which delivers the goods. Fundamental but not-so-simple things like that, familiar to logicians but not necessary to mathematicians (who need to be convinced why, here at least, the should care)!  I think I’m beginning to see how to shape such a chapter to say what needs to be said without getting too tendentious, after some fun reading around for more inspiration. And since I couldn’t see that a few weeks ago, there must have been progress, even if at a snail’s pace.

I’ll put the draft chapter online for comments when it’s done. But some very nice forthcoming events here mean I have to put further work on hold for a bit. So don’t hold your breath.

Posted in Category theory, This and that | 1 Comment

New package for setting proof tableaux

Suppose you want to typeset (using LaTeX of course) a proof tree that looks something like this: Screengrab copy

Maybe that’s an answer to some exercise for students, which is why you want a tree fully annotated with line numbers, justifications on the right, and justifications too for closing off branches. Previously, getting in all that detail using available LaTeX resources would have been tricky. Now help is at hand. There is a very nice new package prooftrees.sty which will enable you to generate that output easily. And, of course, generate simpler results too, without line numbers and/or justifications, if that’s what you want. The package seems very flexible and to provide, at last, the kind of purpose-built-for-logicians tool that we have needed for a long time. So all credit to Clea Rees for her work on this.

Posted in Geek stuff | Leave a comment