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). Is it, however, the best place for most readers to make a first start on the topic? A judgement call, perhaps, but I have to say that I really very much doubt it.

To be continued

Leave a Comment

Your email address will not be published. Required fields are marked *

Scroll to Top