Discussing "Structural Proof Theory"

(Link)

Authors: Sara Negri and Jan von Plato (University of Helsinki)

Reference: Negri, Sara, and von Plato, Jan. Structural proof theory. Cambridge University Press, 2001.

Why this book? Cited by Two-sided Sequent Calculi for FDE-like Four-valued Logics and Proof Theory for Intuitionistic Temporal Logic

There has been an unplanned delay to the blog, as two weeks ago there were not enough new recommendations appearing in Google Scholar to recommend any ‘classic papers’ for me to review via their citations, and then one week ago we got this book, which took me a small while to track down. I therefore expect to post twice this week.

A `structural’ proof is one that proceeds via a set of inference rules that forces one to arrange one’s proof in a tree-like structure, using only a limited set of inference rules and axioms. These inference rules generally reflect the logical connectives used to state the proposition one is trying to prove.  For example, to prove a conjunction one `branches’ to prove each side of the conjunction separately. This may seem a mundane or obvious notion, but is actually very young with respect to the long history of logic, originating with Gerhard Gentzen in the 1930s. The structural approach allows one to study the space of proofs for a given logic as an object of mathematical interest in its own right (hence, proof theory) and can help with finding proofs.

The two important systems for structural proof are natural deduction and sequent calculus, both originating with Gentzen. Natural deduction is intended to reflect the natural way in which one reasons logically, and is an important concept in computer science due to its relationship with types: according to the Curry-Howard isomorphism, programs with a given type can be viewed as natural deduction proofs of a certain proposition, and vice versa. Sequent calculus is a slightly less natural notion where one works on `sequents’ which allow one to manipulate one’s premises as well as one’s conclusion(s). This turns out to be an ideal setting in which to study the space of all proofs for a logic, and can support automated proof search and help to demonstrate that non-theorems are not provable. While the two approaches differ, they also have many similarities; for example, both have a notion of an algorithm (called normalisation or reduction for natural deduction, and cut-elimination for sequent calculus) that automatically simplifies unnecessarily complex or indirect proofs.

This book is a careful development of various notions of natural deduction and sequent calculus for classical, intuitionistic, and intermediate logic, including propositions, predicates, equality, and ‘nonlogical rules’ that give one access to the axioms of various parts of logic. Full proof details are given throughout the book, a number of new results are presented alongside the classic results, and care is taken to place ideas in their historical context. The high level of detail make this a less breezy read than, say, Girard’s Proofs and Types, but it is in invaluable tool to anyone working in the area.