by Dale Miller, INRIA & LIX/Ecole Polytechnique, France
Lectures were divided into two 90 minute sessions. Slides are available: Part 1 | Part 2
Gentzen's sequent calculus is equipped with three kinds of inference rules. The identity rules---cut and initial---can be eliminated except for atomic instances of the initial rule. The introduction rules are the ``atoms'' of inference: they describe how to reason from and reason to logical connectives via their introduction in the left and right sides of sequents. The structural rules of contraction and weakening provide a means to distinguish between proofs in classical, intuitionistic, and minimal logics.
Girard's linear logic has expanded and clarified the relationships between introduction rules and structural rules. In particular, the introduction rules for the propositional connectives come in additive and multiplicative forms. The logic of multiplicative and additive linear logic, MALL, forms an expressive core of logic with decidable provability. MALL can be extended to full linear logic with the addition of the exponentials which mark formulas that can be contracted and weakened and which relate the additives and multiplicatives in the expected way. MALL can also be extended with least and greatest fixed points in order to provide a logic more attuned to arithmetic and inductive reasoning.
In recent years, a new class of sequent calculus proof systems, called focused proof systems, has been used to expand our understanding of how introduction rules and structural rule relate to each other. In these proof systems, inference rules and logical connectives are polarized as negative or positive in such a way that the invertible inference rules all belong to the negative polarity. Groups of negative connectives can then be grouped into one negative synthetic connective: similarly, positive connectives can be grouped into a positive synthetic connective. Such synthetic connectives admit cut-elimination. Remarkably, focused proof systems for classical and intuitionistic logics can be organized so that negative formulas are, in fact, treated linearly. That is, if weakening or contraction is applied to a formula, that formula is positive.
Focused proof systems can be used to design richly varying collections of synthetic connectives. These proof systems also provide for new means of describing parallelism within proofs and mixing computation and deduction. The ability to treat negative formulas linearly provides important information for the design of automated theorem provers. Synthetic connectives and their associated inference rules will also allow for the design of broad spectrum proof certificates that theorem provers will be able to print and simple proof checkers will be able to validate.
In the first part of my lectures, I will cover the basics of sequent calculus, paying particular attention to the role of structural rules. The second part of my lectures will concentrate on the uses of focused proof systems in the proof theory of intuitionistic and classical logic as well as in computer science applications related to inductive theorem proving and model checking.