Peter Smith's Blog, page 40

Big Red Logic Book, no. 2 — a year on

And it is now exactly a year since the self-published version of the second edition of An Introduction to Formal Logic was published as a paperback. This sells about 80 copies a month, very steadily. Again, the figure strikes me as surprisingly high, given that the PDF has also been freely available all along — and that’s downloaded about 850 times a month. Some of the online support materials, like the answers to exercises, are quite well used too. All in all, pretty pleasing.

I occasionally get friendly feedback about the book: and it will be interesting to see if sales/downloads jump at the beginning of the new term/semester as one or two more lecturers adopt the book as a main text. I do hope so (if only because students shouldn’t be being asked to fork out $100 for second-rate course-texts!).

Still, there’s a lot about this book that could be better, so I really do want to have a third bash at an introductory logic text, and sooner rather than later. But I haven’t yet decided quite how to handle this. Something that is recognisably a third edition of the present book? Or, leaving this version out there as it is (apart from any needed corrections), a rather different, brisker book, requiring just a bit more of the reader?  Choices, choices …

 

The post Big Red Logic Book, no. 2 — a year on appeared first on Logic Matters.

An Introduction to Proof Theory, Ch. 6

We are already two hundred pages into IPT: but onwards! We’ve now arrived at Chapter 6, The Cut-Elimination Theorem. Recall, the sequent calculus that Mancosu, Galvan and Zach have introduced is very much Gentzen’s; and now their proof of cut elimination equally closely follows Gentzen.

The story goes like this. The chapter begins by introducing the mix rule, which is easily seen to be equivalent to the cut rule. Suppose then we can establish the Main Lemma that a classical proof with a single mix as its final step can be transformed into a mix-free proof of the same end-sequent. Repeatedly applying the Main Lemma top-down to subproofs of a given proof and we’ll get a mix-free version: and proving the eliminability of mixes like this is enough to establish the cut-elimination theorem.

Then (§6.1) we get some preliminary definitions of the degree and rank of a proof (dependent on the occurrences of mixes), and (§6.2) a strategy for proving the Main Lemma is described — do a double induction on the degree and rank of proofs ending with a single mix. The basic strategy is clearly explained, but working through the proof involves tackling a lot of cases — and our authors insist on laborious completeness “for systematic and pedagogic reasons”. Then §6.3 to 6.5 fill out the detailed proof in twenty-nine(!) pages. §6.6 and §6.7 give examples of degree-lowering and rank-lowering transformations in action. §6.8 notes how the proof for the Gentzen’s classical sequent calculus carries over to the intuitionist case. Then §6.9 pauses to explain why the proof-strategy for establishing mix-elimination doesn’t carry over to a direct proof for cut-elimination (that’s good! — I can’t recall offhand other presentations doing this as explicitly). Then finally, after fifty pages, we get two sections on consequences of cut-elimination.

Page-by-page, this is mostly pretty clear (perhaps not so much in the proof of the midsquent theorem in §6.11). But we aren’t told what the pedagogic reasons are for doing everything this way, in this level of minute detail. Once the strategy for proving the Main Lemma has been outlined, what will the alert reader gain from hacking through nearly thirty pages of detail as opposed to e.g. Takeuti’s six pages of headlines? And tackling Gentzen’s original LK system with sequences rather than multisets either side of the sequent arrow already makes proofs unnecessarily messy. Takeuti wisely makes what really matters in proof transformations vivid by leaving out steps, with placeholders like “some exchanges”: IPT puts in every step so you frequently have to look two or three times to see what matters. Why?

But more basically, why the sole focus on Gentzen’s original sequent calculus when it is well known that revised systems like G3i and G3c lend themselves much more neatly to cut-elimination proofs? Working with those systems you get the essence of what’s going on without unnecessary distractions. Historical piety is all very well in its place; but perhaps its place isn’t in shaping a reader’s first encounter with sequent calculi and their proof theory.

To make the obvious comparison, the first four chapters of von Plato and Negri’s Structural Proof Theory cover the basics of the sequent calculus, with chapters on intuitionist propositional logic (focusing on the propositional version of G3i), classical propositional logic (cut down from G3c), and then the full first-order versions, with cut-elimination theorems for each case snappily proved along the way (the details are  there, but much less painful). There are also discussions of the consequences of cut elimination, and many more asides, all done in a pretty reader-friendly way in twenty-five fewer pages. What’s not to like?

To be continued

The post An Introduction to Proof Theory, Ch. 6 appeared first on Logic Matters.

Big Red Logic Book, no. 1 — a year on

It is exactly a year ago that the self-published version of An Introduction to Gödel’s Theorems was published as a paperback. It has sold over seven hundred copies in that time, and the monthly trend is slowly upwards. That’s three times as many copies as the CUP paperback was selling: but then, this print-on-demand version is a third of the cost! Still, the figure strikes me as surprisingly high, given that the PDF has also been freely available at the same time as the new paperback. I guess that quite a few people, like me, prefer to work from a physical book, if one is available at a modest price. As far as downloads go, AWStats currently reports about five hundred a month — though who knows exactly what these download  stats really mean. And they can be volatile, month by month, though average numbers do stay pretty steady. Anyway, I count that as overall a happy success!

Who knows if I will ever get round to a third edition. There’s tidying to be done, and I’d quite like to add a bit more around and about the Second Theorem. It would be fun to catch up with some reading and re-reading and re-thinking. But I don’t cringe when I occasionally have occasion to glance at the book: so I’m not yet feeling an urgent push to getting back to revising it right now.

The post Big Red Logic Book, no. 1 — a year on appeared first on Logic Matters.

An Introduction to Proof Theory, Ch. 5.

This chapter is on The Sequent Calculus. We meet Gentzen’s LJ and LK, with the antecedents and succedents taken to be sequences of formulas. It is mentioned that some alternative versions treat the sequent arrow as relating sets or multisets so the corresponding structural rules will be different; but it isn’t mentioned that alternative rules for the logical connectives are often proposed, making for some alternative sequent calculi with nice formal features. The definite article in the chapter title could mislead.

And how are we to interpret the sequent arrow? Taking the simplest case with a single formula on each side, we are initially told that A ⇒ B “has the meaning of A ⊃ B” (p. 169). But then later we are told that “we might interpret such a sequent [as A ⇒ B] as the statement that B can be deduced from the assumption A” (p. 192, with letters changed). So which does it express? — a material conditional or a deducibility relation? I vote for saying that the sequent calculus is best regarded as a regimented theory of deducibility!

Now, the conscientious reader of IPT will have just worked through over a hundred pages on natural deduction. So we might perhaps have expected to get next some linking sections explaining how we can see the sequent calculus as in a sense a development from natural deduction systems. I am thinking of the sort of discussion in the very helpful opening chapter ‘From Natural Deduction to Sequent Calculus’ of Jan von Plato and Sara Negri’s Structural Proof Theory (CUP, 2001). At the least, it would be good to ease the student in by starting with some natural deduction proofs and their sequent calculus analogues, to give a sense of how things work. But as it is, after setting up the calculus, IPT dives straight in to consider proof discovery by working back from the desired conclusion, with the attendant complications that arise from using sequences rather than sets or multisets. This messiness at the outset doesn’t seem well calculated to get a student to appreciate the beauty of the sequent calculus! However, the discussion does give some plausibility to the claim that provable sequents should be provable without cut.

A proof of cut elimination is the topic of the next chapter. The rest of this present chapter goes through some more sequent proofs, and proves a couple of lemmas (e.g. one about variable replacement preserving proof correctness). And then there are ten laborious pages showing how an intuitionist natural deduction NJ proof can be systematically transformed into an LJ sequent proof, and vice versa.

The lack of much motivational chat at the beginning of the chapter combined with these extended and less-than-thrilling proofs at the end do, to my mind, make this a rather unbalanced menu for the beginner meeting the sequent calculus for the first time. At the moment, then, I suspect that many such readers will get more out of, and more enjoy, making a start on von Plato and Negri’s book. But does IPT’s Chapter 6 on cut elimination even up the score?

To be continued

The post An Introduction to Proof Theory, Ch. 5. appeared first on Logic Matters.

A Introduction to Proof Theory, Ch. 5.

This chapter is on The Sequent Calculus. We meet Gentzen’s LJ and LK, with the antecedents and succedents taken to be sequences of formulas. It is mentioned that some alternative versions treat the sequent arrow as relating sets or multisets so the corresponding structural rules will be different; but it isn’t mentioned that alternative rules for the logical connectives are often proposed, making for some alternative sequent calculi with nice formal features. The definite article in the chapter title could mislead.

And how are we to interpret the sequent arrow? Taking the simplest case with a single formula on each side, we are initially told that A ⇒ B “has the meaning of A ⊃ B” (p. 169). But then later we are told that ”we might interpret such a sequent [as A ⇒ B] as the statement that B can be deduced from the assumption A” (p. 192, with letters changed). So which does it express? — a material conditional or a deducibility relation? I vote for saying that the sequent calculus is a regimented theory of deducibility!

Now, the conscientious reader of IPT will have just worked through over a hundred pages on natural deduction. So we might perhaps have expected to get next some nice linking sections explaining how we can see the sequent calculus as in a sense a development from natural deduction systems. I am thinking of the sort of discussion in the nice opening chapter ‘From Natural Deduction to Sequent Calculus’ of Jan von Plato and Sara Negri’s Structural Proof Theory (CUP, 2001). At the least, it would be good to ease the student in by starting with some natural deduction proofs and their sequent calculus analogues, to give a sense of how things work. But as it is, after setting up the calculus, IPT dives straight in to consider proof discovery by working back from the desired conclusion, with the attendant complications that arise from using sequences rather than sets or multisets. This messiness at the outset doesn’t seem well calculated to get a student to appreciate the beauty of the sequent calculus! However, the discussion does give some plausibility to the claim that provable sequents should be provable without cut.

Cut elimination is the topic of the next chapter. The rest of this present chapter goes through some more sequent proofs, and proves a couple of lemmas (e.g. one about variable replacement preserving proof correctness). And then there are ten laborious pages showing how an intuitionist natural deduction NJ proof can be systematically transformed into an LJ sequent proof, and vice versa.

The lack of much motivational chat at the beginning of the chapter combined with these extended and less-than-thrilling proofs at the end do, to my mind, make this a rather unbalanced menu for the beginner meeting the sequent calculus for the first time. At the moment, then, I suspect that many such readers will get more out of, and more enjoy, making a start on von Plato and Negri’s book. But does IPT’s Chapter 6 on cut elimination even up the score?

To be continued

The post A Introduction to Proof Theory, Ch. 5. appeared first on Logic Matters.

An Introduction to Proof Theory, Ch. 4

What are we to make of Chapter 4: Normal Deductions? This gives very detailed proofs of normalization, first for the ∧⊃¬∀ fragment of natural deduction, then for the intuitionist system, then for full classical natural deduction, with equally detailed proofs of the subformula property along the way. It all takes sixty seven(!!) pages, often numbingly dense. You wouldn’t thank me for trying to summarize the different stages, though I think things go along fairly conventional lines. I’ll just raise the question of who will really appreciate this kind of very extended treament?

It certainly is possible to introduce this material without mind-blowing tedium. For example, Jan von Plato’s very readable book Elements of Logical Reasoning (CUP 2013) gets across a rich helping of proof theoretic ideas at a reasonably introductory level with some zest, and has a rather nice balance between explanations of general motivations and proof-strategies on the one hand and proof-details on the other. An interested philosophy student with little background in logic who works through the book should come away with a decent initial sense of its topics, and will be able to appreciate e.g. Prawitz’s Natural Deduction. the more mathematical will then be in a position to tackle e.g. Troesltra and Schwichtenberg’s classic with some conceptual appreciation.

Mancosu, Galvan and Zach’s methodical coverage of normalization isn’t, I suppose, much harder than von Plato’s presentation (scattered sections of which appear at different stages of his book); it should therefore be accessible to those who have the patience to plod though the details of their Chapter 4 and who try not to lose sight of the wood for the trees. But I do wonder whether the slow grind here will really produce more understanding of the proof-ideas. I guess that I can recommend the chapter as a helpful supplement for someone who wants to chase up particular details (e.g. because they found some other, snappier, outline of normalization proofs hard to follow on some point). But is it this best place for most readers to make a first start on the topic? I have to say that I really rather doubt it.

To be continued

The post An Introduction to Proof Theory, Ch. 4 appeared first on Logic Matters.

An Introduction to Proof Theory, Ch. 3

Chapter 3 of IPT is on Natural Deduction. The main proof-theoretic work, on normalization, is the topic of the following chapter, and so the topics covered here are relatively elementary ones.

In particular, the first four sections of the chapter simply introduce Gentzen-style proof systems for minimal, intuitionist, and classical logic. So, as with most of the previous chapter, the main question about these sections is: just how good is the exposition?

One initial point. The book, recall, is aimed particularly at philosophy students with only a minimal background in mathematics and logic. But if they are reading this book at all, then — a pound to a penny — they will have done some introductory logic course. And it is quite likely that in this course they will already have met natural deduction done Fitch-style (indenting subproofs in the way expounded in no less than thirty different logic texts aimed at philosophers). It seems strange, to say the least, not to mention Fitch-style natural deduction at all; wouldn’t it have helped many readers to do a compare-and-contrast, explaining why (for proof-theoretic work) Gentzen-style tree layouts are customarily the standard?

An explicit comparison might, indeed, have helped in various places. For example, on p. 73 we are bluntly told that the inference from A to (B ⊃ A) is allowed by the conditional proof rule, i.e. vacuous discharge is allowed. No explanation is given to the neophyte of why this isn’t a cheat. A student familiar with conditional proof in a Fitch-style setting (where there is no requirement that the formula at the head of a subproof is essentially used in the derivation of the end-formula of the subproof) should have a head start in understanding what is going on in the Gentzen setting and why it might be thought unproblematic. Why not make the connection?

Next, it is worth saying that, while this chapter is about natural deduction proofs, there isn’t a single actual example of a proof set out! For the tree arrays which populate the chapter aren’t object language proofs, with formulas as assumptions and a formula as conclusion — they are all entirely schematic, with every featured expression a metalinguistic schema. Ok, this is pretty common practice; and wouldn’t be worth my remarking on if it was very clearly explained that this is what is happening. But it isn’t (I suppose a mis-stated single sentence back on p. 20 in the previous chapter is somehow supposed to do the job). And worse, our authors sometimes seem to themselves forget that everything is schematic. For example, at the foot of p. 79 an attempted proof schema is laid out, ending with the schema 𝐴(𝑐) ⊃ ∀𝑥𝐴(𝑥). This is followed by the comment “The end-formula of this ‘deduction’ is not valid, so it should not have a proof”. But the expression at the end of the proof schema isn’t a formula in the sense defined earlier in the chapter (i.e. it isn’t an object-language wff). And it is formulas, not schemas, that have natural deduction proofs according to the definition of a proof on p. 69. OK, so what is “the end-formula” here? — are they generalizing about all instances of the proof schema? Well, the end-formula of an instance of this attempted proof schema could perfectly well be valid. Ok, yes of course, it is easy to tidy this up so it says what is meant, along with a number of related mishaps: but the student reader shouldn’t be left having to do the work.

A third point. Oddly to my mind, the authors have decided to say nothing here about the supposed harmony between the core introduction and elimination rules shared by classical and intuitionist logic (there is just the briefest of mentions in the Preface of this as a topic that the reader might want to follow up). Well, I can certainly understand not wanting to get embroiled in the ramifying debates about the philosophical significance of harmony. But the relevant formal feature of the intuitionist system is so very neat that it is surely worth saying something about it, even when formal issues are at the forefront of attention. More generally — though I do realize this now is a rather unfocused grumble — I’d say that the expository §§3.1–3.4 don’t really bring out the elegance of Gentzen-style natural deduction.

Moving on to the rest of the chapter, §3.5 notes a couple of measures of the complexity of a deduction tree, and then the remaining two sections of the chapter look at a handful of results about deductions proved by induction on complexity. In particular, §3.7 shows that a formula is deducible in the axiomatic system for classical logic given in the previous chapter if and only if it is deducible in the classical natural deduction system described in this chapter. This bit of proof-theory is nicely done.

I’ve more quibbles that I’ll skip over. But overall, I would say that this chapter does fall somewhat short of my ideal of an introduction to Gentzen-style natural deduction. Still, students coming to it already knowing about Fitch-style proofs will surely be able to manage the transition and should get the hang of things pretty well. But I suspect that those who have never encountered a natural deduction system before might find it all significantly harder going.

To be continued

The post An Introduction to Proof Theory, Ch. 3 appeared first on Logic Matters.

An Introduction to Proof Theory, Ch. 2

IPT is particularly aimed at those “who have only a minimal background in mathematics and logic”. Well, philosophy students who haven’t done much logic may well not have encountered an old-school axiomatic presentation of logic before. So — perhaps reasonably enough — Chapter 2 is on Axiomatic Calculi.  The chapter divides into two uneven parts, which I’ll take in turn.

In the early sections, we meet axiomatic versions of minimal, intuitionist and classical logic for propositional logic (presented using axiom schemas in the usual way). Next, after a pause to explain the idea of proofs by induction, there’s a proof of the deduction theorem, and an explanation of how to prove independence of axioms (more particularly, the independence of ex falso from minimal logic, and the independence of the double negation rule from intuitionist logic) using deviant “truth”-tables. Then we add axioms for predicate logic, and prove the deduction theorem again. So this part of the chapter is routine stuff. And really the only question is: how well does the exposition unfold?

By my lights, not very well. OK, perhaps the general state of the world is rather getting to me, and my mood is less than sunny. But I did find this disappointing stuff.

For a start, the treatment of schemas is a mess. It really won’t do to wobble between saying (p. 19) that axioms are formulas which are instances of schemas, and saying that such a formula is an instance of an axiom (p. 21). Or how about this: “an instance of an instance of an axiom is an axiom” (p. 21). This uses ‘axiom’ in two different senses (i.e. first meaning axiom schema) and then meaning axiom), and it uses ‘instance’ in two different senses (first meaning instance (of schema) and then meaning variant schema got by systematically replacing individual schematic letters by schemas for perhaps non-atomic wffs).

Or how about this? — We are told that a formula is a theorem just if it is the end-formula of a derivation (from no assumptions). We are immediately told, though, that “in general we will prove schematic theorems that go proxy for an infinite number of proofs of their instances.” (p. 20) You can guess what this is supposed to mean: but it isn’t what the sentence actually says. There’s more of the same sort of clumsiness.

When it comes to laying out proofs, things again get messy. The following, for example, is described as a derivation (p. 32):

This is followed by the comment “Note that lines 1 and 2 do not have a ⊢ in front of them. They are assumptions, not theorems. We indicate on the left of the turnstile which assumptions a line makes use of. For instance, line 4 is proved from lines 1 and 3, but line 3 is a theorem — it does not use any assumptions.” But first, with this sort of Lemmon-esque layout, shouldn’t the initial lines have turnstiles after all? Shouldn’t the first line commence, after the line number, with “(1) ⊢” — since the assumption that the line makes use of is itself? And more seriously, in so far we can talk of line (9) as being derived from what’s gone before, it is the whole line read in effect as a sequent which is derived from line (8) read as a sequent — it’s not an individual formula derived from earlier ones by a rule of inference. So in fact this just isn’t a derivation any more in the original sense given in IPT in characterizing axiomatic derivations.

I could continue carping like this but it would get rather boring. However, a careful reader will find more to quibble about in these sections of the chapter, and — more seriously — a student coming to them fresh could far too easily be misled/confused.

The final long §2.15, I’m happy to say, is a rather different kettle of fish, standing somewhat apart from the rest of the chapter in both topic and level/quality of presentation. This section can be treated pretty much as a stand-alone introduction to classical and intuitionist first-order Peano Arithmetic (with an axiomatic logic), which then shows how to interpret the first in the second, thereby establishing that classical PA is consistent if the intuitionist version is. This is, I think, rather neatly done (though I suspect the discussion might need a slightly more sophisticated reader than what’s gone before).

Just one very minor comment. A student might wonder why what is here called the Gödel-Gentzen translation (atoms are left untouched) is different from what many other references call the Gödel-Gentzen translation (where atoms are double negated). A footnote of explanation might have been useful. But as I say, this twelve page section seems much better.

To be continued

The post An Introduction to Proof Theory, Ch. 2 appeared first on Logic Matters.

An Introduction to Proof Theory, Ch. 1

It’s arrived! Ever since it was announced, I’ve been very much looking forward to seeing this new book by Paolo Mancosu, Sergio Galvan and Richard Zach. As they note in their preface, most proof theory books are written at a fairly demanding level. So there is certainly a gap in the market for a book that presents some basic proof theory taking up themes from Gentzen in a more widely accessible way, covering e.g. proof normalization, cut-elimination, and a proof of the consistency of arithmetic using ordinal induction. An Introduction to Proof Theory (OUP, newly published) aims to be that book.

Back in the day, when I’d finished my Gödel book, I had it in mind for a while to write a Gentzen book a bit like IPT (as I’ll refer to it) though a couple of notches more technical. But when I got down to work, I quickly realized that my grip on the area was really quite embarrassingly shallow in places, and I lost all confidence. What I should have done was downsize my ambitions and tried instead to write a book more like this present one. So I have a particular personal interest in seeing how Mancosu, Galvan and Zach write up their project. I’m cheering them on!

Some brisk notes, then, as I read through …

Chapter 1: Introduction has three brisk sections, on ‘Hilbert’s consistency program’, ‘Gentzen’s proof theory’ and ‘Proof theory after Gentzen’.

The scene-setting here is done very cogently and reliably as far as it goes (just as you’d expect). However, on balance I do think that — given the intended readership — the first section in particular could have gone rather more slowly. Hilbert’s program really was a great idea, and a bit more could have been said to  explore and illuminate its attractions. On the other hand, an expanded version of the third section would probably have sat more naturally as a short valedictory chapter at the end of the book.

But then, one thing I’ve learnt from writing my own introductory books is that you aren’t going to satisfy everyone — indeed,  probably not even a majority of your hoped-for readers will be happy. Wherever you set the dial, many will complain that you take things at far too slow a pace, while others will complain that you lost them only a few chapters in. So, in particular, these questions of how much initial scene-setting to provide are very much a judgement call.

To be continued (and I’ll return to The Many and the One in due course).

The post An Introduction to Proof Theory, Ch. 1 appeared first on Logic Matters.

The Chiaroscuro Quartet play Schubert’s Rosamunde

I hadn’t noticed before that there is a video of the Chiaroscuro Quartet playing Schubert’s Rosamunde Quartet from a concert in Gstaad a couple of years ago. Their earlier CD including this piece is wonderful, it goes without saying, but it is terrific to be able to watch them playing in a live performance. (To see the whole recording, you need to register, for free, for the Gstaad Digital Festival.)

The post The Chiaroscuro Quartet play Schubert’s Rosamunde appeared first on Logic Matters.