Chapter 1: From natural deduction to sequent calculus

We first discuss logical languages and rules of inference in general. The rules of natural deduction are presented, where introduction rules are motivated by meaning explanations and elimination rules determined by an inversion principle. A way is found from the rules of natural deduction to those of sequent calculus. Finally, some of the main characteristics of structural proof analysis in sequent calculus are described.

1.1. Logical systems

Logical systems consist of a formal language and a system of axioms and rules for making logical inferences.

(a) Logical languages: Logical languages are usually defined through a set of inductive clauses for well-formed formulas. The idea is that expressions of a formal language are special sequences of symbols from a given alphabet, as generated by the inductive definition. An alternative way of defining formal languages is through systems of categorial grammars. Such grammars are well-known for natural languages, and categorial grammars for formal languages are in use with programming languages, but not so often in logic.

Under the first approach, expressions of a logical language are formulas defined inductively by two clauses: 1. A statement of what the prime formulas are. These are formulas that contain no other formulas as parts. 2. A statement of what the compound formulas are. These are built from other simpler formulas by logical operations and their definition requires reference to arbitrary formulas and how these can be put together with the symbols for operations to give new formulas. Given a formula, we can find out how it was put together from other formulas and a logical operation, where parentheses may be needed in order to indicate the composition uniquely. Then we can find out how the parts were obtained, until we arrive at the prime formulas. Thus, in the end, all formulas consist of atomic formulas, logical operations and parentheses.

We shall define the language of propositional logic:

1. The prime formulas are the atomic formulas denoted by P, Q, R, …, and falsity denoted by ⊥.

2. If A and B are formulas, then the conjunction A&B, disjunction A ∨ B and implication A ⊃ B are formulas.

For unique readability of formulas, the components should always be put in parentheses but in practice these are left out if a conjunction or disjunction is a component of an implication. Often ⊥ is counted among the atomic formulas but this will not work in proof theory. It is best viewed as a zeroplace connective. Negation ∼ A and equivalence A ⊃⊂ B are defined as ∼A = A ⊃ ⊥ and A ⊃⊂ B = (A ⊃ B)&(B ⊃ A).

Expressions of a language should express something, not just be strings of symbols from an alphabet put correctly together. In logic the thing expressed is called a proposition. Often, instead of saying “proposition expressed by formula A” one says simply “proposition A.” There is a longstanding debate in philosophy on what exactly propositions are. When emphasis is on logic, and not on what logic in the end of a philosophical analysis is, one considers expressions in the formal sense and talks about formulas.

In recent literature, the definition of expressions as sequences of symbols is referred to as concrete syntax. Often it is useful to look at expressions from another point of view, that of abstract syntax as in categorial grammar. The basic idea of categorial grammar is that expressions of a language have a functional structure. For example, the sentence John walks is obtained by representing the intransitive verb walk as a function from the category of noun phrases NP to the category of sentences S, in the usual notation for functions, walk : NP → S. John is an element of the category NP and application of the function walk gives as value walk(John), an element of the category of sentences S. One further step of linearization is required to hide the functional structure, to yield the original sentence John walks. In logic and mathematics, no consideration is given to differences produced by this last stage, nor to differences in the grammatical construction of sentences. Since Frege, one considers only the logical content of the functional structure.

We shall briefly look at the definition of propositional logic through a categorial grammar. There is a basic category of propositions, designated Prop. The atomic propositions are introduced as parameters P, Q, R, … with no structure and with the categorizations

P : Prop, Q : Prop, R : Prop, …

and similarly for falsity, ⊥ : Prop. The connectives are two-place functions for forming new propositions out of given ones. Application of the function & to the two arguments A and B gives the proposition &(A, B) as value, and similarly for ∨ and ⊃. The functional structure is usually hidden by an infix notation and by the dropping of parentheses, A&B for &(A, B), and so on. This will create an ambiguity not present in the purely functional notation, such as A&B ⊃ C that could be both &(A, ⊃ (B, C)) and ⊃ (&(A, B), C). As mentioned, we follow the convention of writing A&(B ⊃ C) for the former and A&B ⊃ C for the latter, and in general, having conjunction and disjunction bind stronger than implication.

Given an arbitrary proposition A, it is either the constant proposition ⊥, an atomic proposition, or (the value of) conjunction, disjunction, or implication. The notation often used in categorial grammar is

A := ⊥ | P | A&B | A ∨ B | A ⊃ B

Appendix A explains in more detail how logical languages are treated from the point of view of categorial grammar.

Neither approach, inductive definition of strings of symbols, or generation of expressions through functional application, reveals what is special about logical languages. Logical languages of the present day have arisen as an abstraction from the informal language of mathematics. The first work in this direction was by Frege who invented the language of predicate logic. It was meant to be, wrote Frege, “a formula language for pure thought, modelled upon that of arithmetic.” Later Peano and Russell developed the symbolism further, with the aim of formalising the language of mathematics. These pioneers of logic tried to give definitions of what logic is, how it differs from mathematics, and whether the latter is reducible to the former, or if it is perhaps the other way around.

From a practical point of view there is a clear understanding of what logical languages are: The prime logical languages are those of propositional and predicate logic. Then there are lots of other logical languages more or less related to these. Logic itself is, from this point of view, what logicians study and develop. Any general definition of logic and logical languages should respect this situation.

An essential aspect of logical languages is that they are formal languages, or can easily be made into such, an aspect made all the more important by the development of computer science. There are many connections between logical languages and programming languages; in fact, logical and programming languages are brought together in one language in some recent developments as explained in Appendix B.

(b) Rules of inference: Rules of inference are of the form:“If it is the case that A and B, then it is the case that C.” Thus, they do not act on propositions, but on assertions. We obtain an assertion from a proposition A by adding something to it, namely an assertive mood such as “it is the case that A.” Frege used the assertion sign ⊢ A to indicate this but usually the distinction between propositions and assertions is left implicit. Rules seemingly move from given propositions to new ones.

In Hilbert-style systems, also called axiomatic systems, we have a number of basic forms of assertion, like ⊢ A ⊃ A ∨ B or ⊢ A ⊃ (B ⊃ A). Each instance of these forms can be asserted, and in the case of propositional logic there is just one rule of inference, of the form

\begin{matrix}⊢ A ⊃ B & ⊢ A \\ ⊢ B \end{matrix}

Derivations start with instances of axioms that are decomposed by the rule until the desired conclusion is found.

In natural deduction systems, there are only rules of inference, plus assumptions to get derivations started, exemplified by

\begin{matrix}⊢ A & ⊢ B \\ ⊢ A&B \end{matrix}  [⊢ A] ; ⋮ . ; ⊢ B ; ⊢ A ⊃ B

Instances of the first rule are single-step inferences, and if the premisses have been derived from some assumptions, the conclusion depends on the same assumptions. In the second rule instead, where the vertical dots indicate a derivation of ⊢ B from ⊢ A, the assumption ⊢ A is discharged at the inference line, as indicated by the square brackets, so that ⊢ B above the inference line depends on ⊢ A whereas ⊢ A ⊃ B below it does not.

In sequent calculus systems, there are no temporary assumptions that would be discharged, but an explicit listing of the assumptions the derived assertion depends on. The derivability relation, to which reference was made in natural deduction by the four vertical dots, is an explicit part of the formal language and sequent calculus can be seen as a formal theory of the derivability relation.

Of the three types of systems the first, axiomatic, has some good properties due to the presence of only one rule of inference. But it is next to impossible to actually use the axiomatic approach, due to the difficulty of finding the instances of axioms to start with. Systems of the second type correspond to the usual way of making inferences in mathematics, with a good sense of structure. Systems of the third type are the ones that permit the most profound analysis of the structure of proofs, but their actual use requires some practice. Moreover, the following is possible in natural deduction and in sequent calculus:

Two systems of rules can be equivalent in the sense that the same assertions can be derived in them, but the addition of the same rule to each system can destroy the equivalence.

This lack of modularity will not occur with the axiomatic Hilbert-style systems.

Once a system of rules of logical inference has been put up it can be considered from the formal point of view. The assertion sign is left out and rules of inference are just ways of writing a formula under any formula or formulas that have the form of the premisses of the rules. In a complete formalization of logic, also the formation of propositions is presented as the application of rules of proposition formation. For example, conjunction formation is application of the rule

A : Prop B : Prop
A&B : Prop

Rules of inference can be formalized in the same way as rules of proposition formation: They are represented as functions taking as arguments formal proofs of the premisses and giving as value a formal proof of the conclusion. A hierarchy of functional categories is obtained such that all instances of rules of proposition formation and of inference come out through functional application. This will lead to constructive type theory and will be described in more detail in Appendix B.

The viewpoint of proof theory is that logic is the theory of correct demonstrative inference. Inferences are analyzed into the most basic steps the formal correctness of which can be easily controlled. Moreover, the semantical justification of inferences can be made compositional, through the justification of the individual steps of inference and how they are put together.

Compound inferences are synthesized by composing basic steps of inference. A system of rules of inference is used to give an inductive, formal definition of the notion of derivation. Derivability then means the existence of a derivation. The correctness of a given derivation can be mechanically controlled through its inductive definition, but the finding of derivations typically is a different matter.

1.2. Natural deduction

Natural deduction embodies the operational or computational meaning of the logical connectives and quantifiers. The meaning explanations are given in terms of the immediate grounds for asserting a proposition of corresponding form. There can be other, less direct grounds, but these should be reducible to the former for a coherent operational semantics to be possible. The “BHK-conditions” (for Brouwer-Heyting-Kolmogorov) that give the explanations of logical operations of propositional logic in terms of direct provability of propositions, can be put as follows:

1. A direct proof of the proposition A&B consists of proofs of the propositions A and B.

2. A direct proof of the proposition A ∨ B consists of a proof of the proposition A or a proof of the proposition B.

3. A direct proof of the proposition A ⊃ B consists of a proof of the proposition B from the assumption that there is a proof of the proposition A.

4. A direct proof of the proposition ⊥ is impossible.

In the third case it is only assumed that there is a proof of A, but the proof of the conclusion A ⊃ B does not depend on this assumption temporarily made in order to reduce the proof of B into a proof of A. Proof here is an informal notion. We shall gradually replace it by the formal notion of derivability in a given system of rules.

We can now make more precise the idea that rules of inference act on assertions. Namely, an assertion is warranted if there is a proof available and therefore, on a formal level, rules of inference act on derivations of the premisses, to yield as value a derivation of the conclusion. From the BHK-explanations, we arrive at the following introduction rules:

\begin{matrix}A & B \\ A&B \end{matrix}^{&I}  {A \atop A ∨ B}^{∨I1}  {B \atop A ∨ B}^{∨I2}  [A] ; ⋮ . ; B ; A ⊃ B^{⊃I}

The assertion signs are left out. (There will be another use for the symbol soon.) In the last rule the auxiliary assumption A is discharged at the inference, which is indicated by putting it in square brackets. We have as a special case of implication introduction, with B = ⊥, an introduction rule for negation. There is no introduction rule for ⊥.

There will be elimination rules corresponding to the introduction rules. They have a proposition of one of the three forms, conjunction, disjunction or implication as a major premiss. There is a general principle that helps find the elimination rules: We ask what the conditions are, in addition to assuming the major premiss derived, that are needed to satisfy the following

Inversion principle: Whatever follows from the direct grounds for deriving a proposition, must follow from that proposition.

For conjunction A&B, the direct grounds are that we have derivations of A and of B. Given that C follows when A and B are assumed, we thus find through the inversion principle the elimination rule

\begin{aligned}A&B & & [A, B] ; ⋮ . ; C \\ & C \end{aligned}^{&E}

The assumptions A and B from which C was derived, are discharged at the inference. If in a derivation the premisses A and B of the introduction rule have been derived and C has been derived from A and B, the derivation

\begin{matrix}\begin{matrix}⋮ . ; A & ⋮ . ; B \\ A&B \end{matrix}^{&I} & [A, B] ; ⋮ . ; C \\ C \end{matrix}^{&E}

converts into a derivation of C without the introduction and elimination rules,

⋮ . ; A ⋮ . ; B ; ⋮ . ; C

Therefore, if &I is followed by &E, the derivation can be simplified.

For disjunction, we have two cases. Either A ∨ B has been derived from A, and C is derivable from assumption A, or it has been derived from B and C is derivable from assumption B. Taking into account that both cases are possible, we find the elimination rule

\begin{aligned}A ∨ B & [A] ; ⋮ . ; C & [B] ; ⋮ . ; C \\ & C \end{aligned}^{∨E}

Assume now that A or B has been derived. If it is the former and if C is derivable from A and C is derivable from B, the derivation

\begin{matrix}⋮ . ; A ; A ∨ B^{∨I1} & [A] ; ⋮ . ; C & [B] ; ⋮ . ; C \\ C \end{matrix}^{∨E}

converts into a derivation of C without the introduction and elimination rules,

⋮ . ; A ; ⋮ . ; C

In the latter case of B having been derived, the conversion is into

⋮ . ; B ; ⋮ . ; C

Again, an introduction followed by the corresponding elimination can be removed from the derivation.

The elimination rule for implication is harder to find. The direct ground for deriving A ⊃ B is the existence of a hypothetical derivation of B from the assumption A. The fact that C can be derived from the existence of such a derivation, can be expressed by:

If C follows from B, then it already follows from A.

Precisely this is achieved by the elimination rule

\begin{aligned}A ⊃ B & & A & [B] ; ⋮ . ; C \\ & C \end{aligned}^{⊃E}

In addition to the major premiss A ⊃ B, there is the minor premiss A in the ⊃E rule. If B has been derived from A and C from B, the derivation

\begin{matrix}[A] ; ⋮ . ; B ; A ⊃ B^{⊃I} & ⋮ . ; A & [B] ; ⋮ . ; C \\ C \end{matrix}^{⊃E}

converts into a derivation of C from A without the introduction and elimination rules,

⋮ . ; A ; ⋮ . ; B ; ⋮ . ; C

Finally we have the zero-place connective ⊥ that has no introduction rule. The immediate grounds for deriving ⊥ are empty and we obtain as a limiting case of the inversion principle the rule of falsity elimination (“ex falso quodlibet”) that has only the major premiss ⊥:

{⊥ \atop C}^{⊥E}

We have still to tell how to get derivations started. This is done by the rule of assumption that permits us to begin a derivation with any formula. In a given derivation tree, those formula occurrences are assumptions, or more precisely, open assumptions, that are neither conclusions nor discharged by any rule. Discharged assumptions are also called closed assumptions.

The rules &E and ⊃E are usually written only for the special cases of C = A and C = B for &E, and C = B for ⊃E, as follows:

{A&B \atop A}^{&E1}  {A&B \atop B}^{&E2}  \begin{matrix}A ⊃ B & A \\ B \end{matrix}^{⊃E}  (SE)

These “special elimination rules” correspond to a more limited inversion principle, one requiring that elimination rules conclude the immediate grounds for deriving a proposition instead of arbitrary consequences of these grounds. The first two rules just conclude the premisses of conjuntion introduction. The third gives a one-step derivation of B from A. The more limited inversion principle suffices for justifying the special elimination rules but is not adequate for determining what the elimination rules should be. In particular, it says nothing about ⊥E.

The special elimination rules have the property that their conclusions are immediate subformulas of their premisses. With conjunction introduction, it is the other way around, the premisses are immediate subformulas of the conclusion. Further, in implication introduction, the formula above the inference line is an immediate subformula of the conclusion. It can be shown that derivations with conjunction and implication introduction and the special elimination rules can be transformed into a normal form. The transformation is done by detour conversions, the removal of applications of introduction rules followed by corresponding elimination rules. In a derivation in normal form, first assumptions are made, then elimination rules are used, and last introduction rules. This simple picture of normal derivations, moving by elimination rules from assumptions to immediate subformulas and then by introductions the other way around, is lost with the disjunction elimination rule. But we shall show in Chapter 8 that when all elimination rules are formulated in the general form, a uniform subformula property for natural deduction derivations follows.

The conjunction and disjunction introduction rules, as well as the special elimination rules for conjunction and implication (SE), are simple one-step inferences. The rest of the rules are schematic, with “vertical dots” indicating derivations with assumptions. The behaviour of these assumptions is controlled by discharge functions: Each assumption gets a number and the discharge of assumptions is indicated by writing the number next to the inference line. Further, the discharge is optional, i.e., we can, and indeed some times must, leave an assumption open even if it could be discharged.

Some examples will illustrate the management of assumptions and point at some peculiarities of natural deduction derivations. Consider

Example 1:

[A]^{1.} ; A ⊃ A^{⊃I,1.}

The rule schemes of natural deduction only display the open assumptions that are active in the rule, but there may be any number of other assumptions. Thus, the conclusion may depend on a whole set Γ of assumptions, which can be indicated by using the notation Γ ⊢ A. Now the rule of implication introduction can be written as

{Γ ⊢ B \atop Γ − \{A\} ⊢ A ⊃ B}^{⊃I}

In words, if there is a derivation of B from the set of open assumptions Γ, there is a derivation of A ⊃ B from assumptions Γ minus {A}. In this formulation there is a “compulsory” discharge of the assumption A. All the other rules of natural deduction can be written similarly; We give two examples:

\begin{matrix}Γ ⊢ A & Δ ⊢ B \\ Γ ∪ Δ ⊢ A&B \end{matrix}^{&I}  \begin{aligned}Γ ⊢ A ∨ B & Δ ∪ \{A\} ⊢ C & Θ ∪ \{B\} ⊢ C \\ & Γ ∪ Δ ∪ Θ ⊢ C \end{aligned} ^{∨E}

The resulting system of inference, introduced by Gentzen in 1936, is usually known as “natural deduction in sequent calculus style.” It can be used to clarify the strange-looking derivation of example 1: The assumption of A is written as A ⊢ A and we have the derivation

{A ⊢ A \atop ⊢ A ⊃ A}^{⊃I}

The first occurrence of A has the set of assumptions Γ = {A}, and so (dropping for good curly brackets around singleton sets), the conclusion has the set of assumptions A − A = ∅.

The next example shows how superfluous assumptions can be added, to weaken the consequent A of the first example into B ⊃ A:

Example 2:

\begin{matrix}[A]^{1.} ; B ⊃ A & ⊃I \\ A ⊃ (B ⊃ A) \end{matrix}^{⊃I,1.}

The first inference step is justified by the rule about sets of assumptions: A − B = A. There is a vacuous discharge of B in the first instance of ⊃I and discharge of A only takes place at the second instance of ⊃I. Note that there is a problem here in the case of B = A, for compulsory discharge dictates that A is discharged at the first inference, the second becoming a vacuous discharge. The instance of the derivation where B = A is not a syntactically correct one, therefore the original derivation cannot be correct, either. Chapter 8 will give a method for handling the discharge of assumptions, the unique discharge principle, that does not lead to such problems.

In sequent calculus style, the derivation is

\begin{matrix}{A ⊢ A \atop A ⊢ B ⊃ A} & ⊃I \\ ⊢ A ⊃ (B ⊃ A) \end{matrix}^{⊃I}

The next example gives a derivation that cannot be done with just a single use of the assumption A:

Example 3:

\begin{matrix}\begin{matrix}\begin{matrix}[A ⊃ (A ⊃ B)]^{2.} & [A]^{1.} \\ A ⊃ B \end{matrix}^{⊃E} & [A]^{1.} \\ B \end{matrix} & ⊃E \\ A ⊃ B \end{matrix}_{⊃I,1.} ; (A ⊃ (A ⊃ B)) ⊃ (A ⊃ B)_{⊃I,2.}

Assumption A had to be made twice and there is correspondingly a multiple discharge at the first instance of ⊃I where both occurrences of assumption A are discharged. Note the “nonlocality” of derivations in natural deduction: To control the correctness of inference steps where assumptions can be discharged, we have to look higher up along derivation branches. (This will be crucial later with the variable restrictions in quantifier rules.) In sequent calculus style, instead, each step of inference is local:

\begin{matrix}\begin{matrix}\begin{matrix}A ⊃ (A ⊃ B) ⊢ A ⊃ (A ⊃ B) & A ⊢ A \\ A ⊃ (A ⊃ B), A ⊢ A ⊃ B \end{matrix}^{⊃E} & A ⊢ A \\ A ⊃ (A ⊃ B), A ⊢ B \end{matrix} & ⊃E \\ A ⊃ (A ⊃ B) ⊢ A ⊃ B \end{matrix}_{⊃I} ; ⊢ (A ⊃ (A ⊃ B)) ⊃ (A ⊃ B)_{⊃I}

In implication elimination, a rule with two premisses, the assumptions from the left of the turnstile are collected together. At the second implication elimination of the derivation, a second occurrence of A in the assumption part is produced. The trace of this repetition disappears, however, when assumptions are collected into sets.

The above system of introduction and elimination rules for &, ∨ and ⊃, together with the rule of assumption by which an assumption can be introduced at any stage in a derivation, is the system of natural deduction for minimal propositional logic. If we add to it ⊥E we have a system of natural deduction rules for intuitionistic propositional logic.

Classical propositional logic is obtained by adding to the rules of intuitionistic logic a rule we call the rule of excluded middle, in analogy to the law of excluded middle characteristic of classical logic in an axiomatic approach:

\begin{aligned}[A] ; ⋮ . ; C & & [∼A] ; ⋮ . ; C \\ & C \end{aligned}^{Em}

Both A and ∼A are discharged at the inference. The law of excluded middle, A∨ ∼A, is derivable with the rule:

\begin{matrix}{[A] \atop A∨ ∼A}^{∨I1} & {[∼A] \atop A∨ ∼A}^{∨I2} \\ A∨ ∼A \end{matrix}_{Em}

The rule of excluded middle is a generalization of the rule of indirect proof (“reductio ad absurdum”),

[∼A] ; ⋮ . ; ⊥ ; A^{Raa}

The properties of the classical rules Em and Raa are presented in Chapter 8.

Rules of natural deduction can be categorized in a way similar to rules of proposition formation. This is based on the propositions-as-sets principle, and leads to type systems. We think of a proposition A as being the same as its set of formal proofs. Each such proof can be called a proof-object or proof term, to emphasize that this special notion of proof is intended. Instead of an assertion of form ⊢ A we have a : A, a is a proof-object for A. Rules of inference are categorized as functions operating on proof-objects.

Type-theoretical rules for proof-objects validate the BHK-explanations, by showing how proof-objects of compound propositions are constructed from proof-objects of their constituents. For example, the proof of an implication A ⊃ B is a function that converts an arbitrary proof of A into some proof of B. In earlier times, the explanation of a proof of an implication A ⊃ B was described as “a method that converts proofs of A into proofs of B,” and this was thought to be circular or at least ill-founded through its reference to an arbitrary proof of A. But in constructive type theory, the problem is solved.^{1} The meaning explanations first concern only “canonical proofs,” that is, the direct proofs of the forms given by the introduction rules. All other, “non-canonical proofs,” are reduced to the canonical ones through computation rules that correspond to the conversions in natural deduction. For this process to be well-founded, it is required that the conversion from non-canonical to canonical form terminates. These notions have deep connections to the structural properties of natural deduction derivations.

An exposition of type theory and its relation to natural deduction is given in Appendix B.

1The explanation was rejected on these grounds by Gödel (1941), for example. The solution was given, in philosophical terms, by Dummett (1975), and more formally by Martin-Löf (1975).

1.3. From natural deduction to sequent calculus

If our task is to derive A ⊃ B, the rule ⊃I reduces the task to one of deriving B under the assumption A. So we assume A, but if B in turn is of form C&D, the &I rule shows how the derivation of C&D is reduced to that of C and D. Thus we have to mentally decompose the goal A ⊃ B into subgoals, but there is no formal way to keep track of the process. It is as if we had to construct a derivation backwards.

Sequent calculus corrects the lack of guidance of natural deduction. It has a notation for keeping track of open assumptions, moreover, this is local: Each formula C has the open assumptions Γ it depends on listed on the same line, as follows:

Γ ⇒ C

Sequent calculus is a formal theory of the derivability relation. To make a difference to writing Γ ⊢ C, where the turnstile is a meta-level expression, not part of the syntax as are the formulas, we use the now common symbol ⇒. In Γ ⇒ C, the left side Γ is called the antecedent and C the succedent.

As mentioned, the rules of natural deduction are schematic and only show the active formulas, leaving implicit the set of remaining open assumptions. For example, the rule of conjunction introduction can be written more completely as follows, with a derivation of A with open assumptions Γ and a derivation of B with open assumptions Δ:

\begin{matrix}Γ ⋮ . ; A & Δ ⋮ . ; B \\ A&B \end{matrix}^{&I}

Rule &I gives a derivation of A&B with open assumptions Γ ∪ Δ. With implication, we have a derivation of B from A and Γ, and the introduction rule gives a derivation of A ⊃ B from Γ. Similarly with E-rules, for example, disjunction elimination gives a derivation of C from A ∨ B, Γ, Δ, Θ if C is derived from A, Δ and from B, Θ. The management of sets of assumptions was already made explicit in the rules of natural deduction written in sequent calculus style. Sequent calculus maintains the introduction rules thus written, but the treatment of elimination rules is profoundly different.

The rules of sequent calculus are ordered in the same way as those of natural deduction, with the conclusion at the root. The introduction rules of natural deduction become right rules of sequent calculus, where a comma replaces set-theoretical union:

\begin{matrix}Γ ⇒ A & Δ ⇒ B \\ Γ, Δ ⇒ A&B \end{matrix}^{R&} {A, Γ ⇒ B \atop Γ ⇒ A ⊃ B}^{R⊃} {Γ ⇒ A \atop Γ ⇒ A ∨ B}^{R∨_{1}} {Γ ⇒ B \atop Γ ⇒ A ∨ B}^{R∨_{2}}

Rule R⊃ can also be read “root-first” and in this direction it shows how the derivation of an implication reduces to its components. By reduction is here meant that the premiss is derivable just in case the conclusion is.

In Gentzen’s original formulation of 1934–35, the assumptions Γ, Δ, Θ were finite sequences, or lists as we would now say.^{2} Gentzen had rules permitting the exchange of order of formulas in a sequence. But matters are simplified if we consider assumptions finite multisets, that is, lists with multiplicity but no order, and we shall do so from now on. Example 3 of Section 1.2 showed that if assumptions are treated simply as sets, control is lost over the number of times an assumption is made.

The elimination rules of natural deduction correspond to left rules of sequent calculus. In &E, we have a derivation of C from A, B and some assumptions Γ, and we conclude that C follows from A&B and the assumptions Γ. In sequent calculus, this is written as

{A, B, Γ ⇒ C \atop A&B, Γ ⇒ C} ^{L&}

The remaining two left rules are found similarly:

\begin{matrix}A, Γ ⇒ C & B, Δ ⇒ C \\ A ∨ B, Γ, Δ ⇒ C \end{matrix} ^{L∨}  \begin{matrix}Γ ⇒ A & B, Δ ⇒ C \\ A ⊃ B, Γ, Δ ⇒ C \end{matrix} ^{L⊃}

The formula with the connective in a rule is the principal formula of that rule and its components in the premisses the active formulas. The Greek letters denote possible additional assumptions that are not active in a rule; They are called the contexts of the rules.

In natural deduction elimination rules written in sequent calculus style, a formula disappears from the right, in sequent calculus, the same formula appears on the left. Inspection of sequent calculus rules shows what the effect of this change is:

2Use of the word “sequent” as a noun was begun by Kleene. His Introduction to Metamathematics of 1952 (p. 441) explains the origin of the term as follows:“Gentzen says ‘Sequenz’, which we translate as ‘sequent’, because we have already used ‘sequence’ for any succession of objects, where the German is ‘Folge’.” This is the standard terminology now; Kleene’s usage has even been adopted to some other languages. But Mostowski (1965) for example uses the literal translation “sequence.”

Subformula property: All formulas in a sequent calculus derivation are subformulas of the endsequent of the derivation.

The usual way to find derivations in sequent calculus is a “root-first proof search.” But in rules with two premisses, we do not know how the context in the conclusion should be divided between the antecedents of the premisses. Therefore we do not divide it at all but repeat it fully in both premisses. The procedure can be motivated as follows: If in the conclusion assumptions Γ are permitted, it cannot harm to make the same assumptions elsewhere in the derivation. Rules R&, L∨ and L⊃ can be modified into

\begin{matrix}Γ ⇒ A & Γ ⇒ B \\ Γ ⇒ A&B \end{matrix}^{R&}  \begin{matrix}A, Γ ⇒ C & B, Γ ⇒ C \\ A ∨ B, Γ ⇒ C \end{matrix} ^{L∨}  \begin{matrix}Γ ⇒ A & B, Γ ⇒ C \\ A ⊃ B, Γ ⇒ C \end{matrix} ^{L⊃}

The earlier two-premiss rules had independent contexts, the above rules instead have shared contexts.^{3} It now follows that given the endsequent to be derived, once it is decided which formula of the endsequent is principal, the premisses are uniquely determined.

To show how derivations are found in sequent calculus, we derive the sequent

⇒ (A ⊃ (A ⊃ B)) ⊃ (A ⊃ B)

corresponding to example 3 of Section 1.2:

\begin{matrix}A ⇒ A & \begin{matrix}A ⇒ A & B, A ⇒ B \\ A ⊃ B, A ⇒ B \end{matrix}^{L⊃} \\ A ⊃ (A ⊃ B), A ⇒ B \end{matrix}_{L⊃} ; A ⊃ (A ⊃ B) ⇒ A ⊃ B_{R⊃} ; ⇒ (A ⊃ (A ⊃ B)) ⊃ (A ⊃ B)_{R⊃}

Both instances of the two-premiss rule L⊃ have the shared context A. This root-first proof search is not completely deterministic: The last step can only be R⊃, but above that, there are choices in the order of application of rules. Further, proof search need not stop, but we stopped when we reached sequents with the same formula in the antecedent and succedent. Namely, the rule of assumption of natural deduction, by which we can start a derivation with any formula A as assumption, is given in sequent calculus in the form of a logical axiom:

A ⇒ A

3Lately some authors have called these “additive” and “multiplicative” contexts but these are not so easy to remember

In the above derivation, proof search ended in one case with a sequent of form A, Γ ⇒ A, with a superfluous extra assumption. Its presence was caused by the repetition of formulas in premisses when shared contexts are used.

The ⊥E rule of natural deduction gives the zero-premiss sequent calculus rule

⊥ ⇒ C ^{L⊥}

Often this rule is also referred to as an axiom, but we want to emphasize its character as a left rule and do not call it so.

Formally, a sequent calculus derivation is defined inductively: Instances of axioms are derivations, and if instances of premisses of a rule are conclusions of derivations, application of the rule will give a derivation. Thus, sequent calculus derivations always begin with axioms or L⊥. But we depart in two ways from this “official” order of things:

First, note that the logical rules themselves are not derivations, for they have sequents as premisses that need not be axioms. The combination of logical rules likewise gives sequent calculus derivations with premisses. Each logical rule and each combination is correct in the sense that, given derivations of the premisses, the conclusion of the rule or of the combination becomes derivable.

Secondly, the usual root-first proof search procedure runs counter to the inductive generation of sequent calculus derivations. Proof search only succeeds when these two meet, i.e., when the root-first process reaches axioms or instances of L⊥.

We now come to the structural rules of sequent calculus. In order to derive the sequent ⇒ A ⊃ (B ⊃ A) corresponding to example 2 in Section 1.2, we use a rule of weakening introducing an extra assumption in the antecedent:

{Γ ⇒ C \atop A, Γ ⇒ C}^{Wk}

The rule is sometimes called “thinning.” The derivation of example 2 is

\begin{matrix}{A ⇒ A \atop A, B ⇒ A} & Wk \\ A ⇒ B ⊃ A \end{matrix}_{R⊃} ; ⇒ A ⊃ (B ⊃ A)_{R⊃}

The derivation illustrates the role of weakening: Whenever in a natural deduction derivation there is a vacuous discharge, there is in a corresponding sequent calculus derivation an instance of a logical rule with an active formula that has been introduced in the derivation by weakening.

As noted, our example of proof search in sequent calculus led to a premiss that was not an axiom of the form A ⇒ A, but of the form A, Γ ⇒ A. These more general axioms are obtained from A ⇒ A by repeated application of weakening. If instead we permit instances of axioms as well as the L⊥ rule to have an arbitrary context Γ in the antecedent, there is no need for a rule of weakening in sequent calculus.

Above we gave a derivation of the sequent corresponding to example 3 of Section 1.2 using rules with shared contexts. We give another derivation, this time with the earlier rules having independent contexts. A rule of contraction is now needed:

{A, A, Γ ⇒ C \atop A, Γ ⇒ C}^{Ctr}

With this rule and axioms of form A ⇒ A, the derivation is

\begin{matrix}A ⇒ A & \begin{matrix}A ⇒ A & B ⇒ B \\ A ⊃ B, A ⇒ B \end{matrix}^{L⊃} \\ A ⊃ (A ⊃ B), A, A ⇒ B \end{matrix}_{L⊃} ; A ⊃ (A ⊃ B), A ⇒ B_{Ctr} ; A ⊃ (A ⊃ B) ⇒ A ⊃ B_{R⊃} ; ⇒ (A ⊃ (A ⊃ B)) ⊃ (A ⊃ B)_{R⊃}

Contrary to the derivation with shared contexts, a duplication of A is produced on the fourth line from below. The meaning of contraction can be explained in terms of natural deduction: Whenever there is a multiple discharge in natural deduction, there is a contraction in a corresponding sequent calculus derivation.

If assumptions are treated as sets instead of multisets, contraction is in a way built into the system and cannot be expressed as a distinct rule.

As with weakening, the rule of contraction can be dispensed with, by the use of rules with shared contexts and some additional modifications.

In Chapter 8 we show in a general way that weakening and contraction amount to vacuous and multiple discharge, respectively, in natural deduction, whenever the weakening or contraction formula is active in a derivation. Without this condition, weakening and contraction are purely formal matters produced by the separation of discharge of assumptions into independent structural and logical steps in sequent calculus.

We now come to the last and most important general rule of sequent calculus: Given two natural deduction derivations Γ ⊢ A and A, Δ ⊢ C, we can join them together into a derivation Γ, Δ ⊢ C, through a substitution. The sequent calculus rule corresponding to this is cut:

\begin{matrix}Γ ⇒ A & A, Δ ⇒ C \\ Γ, Δ ⇒ C \end{matrix}^{Cut}

Often cut is explained as follows: We break down the derivation of C from some assumptions into “lemmas,” intermediate steps that are easier to prove and that are chained together in the way shown by the cut rule. In Chapter 8 we find a somewhat different explanation of cut: It arises, in terms of natural deduction, from non-normal instances of elimination rules.

It is possible that the derivations Γ ⊢ A and A, Δ ⊢ C in a given system of rules of inference can be brought into a normal form, but the derivation Γ, Δ ⊢ C obtained by cut need not, in general, have any such form.

Weakening, contraction and cut are the usual structural rules of sequent calculus. Cut has the effect of making a formula disappear during a derivation so that it is not a subformula of the conclusion, whereas none of the other rules does this. If we wanted to determine whether a sequent Γ ⇒ C is derivable, using cut we could always try to reduce the task into Γ ⇒ A and A, Γ ⇒ C with a new formula A, with no end.

A main task of structural proof theory is to find systems that do not need the cut rule, or only use it in some limited way. But note that contraction can be as “bad” as cut, as concerns a root-first search for a derivation of a given sequent: Formulas in antecedents can be multiplied with no end if contraction cannot be dispensed with.

Two main types of sequent calculi arise: Those with independent contexts, similar in many respects to calculi of natural deduction, and those with shared contexts, useful for proof search. Gentzen’s original (1934–35) calculi for intuitionistic and classical logic had shared contexts for R& and L∨, and independent ones for L⊃. Further, the left rule for & (as well as the R∨ rule in the classical case) was given in the form of two rules

{A, Γ ⇒ C \atop A&B, Γ ⇒ C}  {B, Γ ⇒ C \atop A&B, Γ ⇒ C}

that do not support proof search: It need not be the case that A, Γ ⇒ C is derivable even if A&B, Γ ⇒ C is. The single L& rule we use is due to Ketonen (1944). He also improved the classical R∨ rule in an analogous way and found a classical L⊃ rule with shared contexts. With these changes, the sequent calculus for classical propositional logic is invertible: From the derivability of a sequent of any of the forms given in the conclusions of the logical rules, the derivability of its premisses follows. Starting with the endsequent, decomposition by invertible rules gives a terminating method of proof search for classical propositional logic.

For intuitionistic logic, a sequent calculus with shared contexts was found by Kleene (1952). The rule of cut can be eliminated in calculi with independent as well as shared contexts. In calculi of the latter kind, also weakening and contraction can be eliminated, so that derivations contain logical rules only. Most of Chapters 2–4 is devoted to the development and study of such calculi. Calculi with independent contexts are studied in Chapter 5.

1.4. The structure of proofs

Given a system of rules G, we say that a rule with premisses S_{1}, …, S_{n} and conclusion S is admissible in G if, whenever an instance of S_{1}, …, S_{n} is derivable in G, the corresponding instance of S is derivable in G. Structural proof theory has as its first task the study of admissibility of rules such as weakening, contraction and cut. Our methods for establishing such results will be thoroughly elementary: In part we show that the addition of a structural rule has no effect on derivability (as for weakening), or we give explicit transformations of derivations using structural rules into ones that do not use them (as for cut). A major difficulty is to find the correct rules in the first place. Even if the proof methods are all elementary, the proofs often depend on the right combination of many details and are much easier to read than write.

Gentzen spoke about the elimination of cut. A related notion is closure under cut: If we have a complete system that does not contain cut, we can conclude that derivable sequents are derivable without cut. But this is a weaker notion than cut elimination, since one only has the semantical proof of completeness, not necessarily a process of effectively eliminating cuts from a given derivation.

If the cut rule has been shown admissible for a system of rules, we see by inspection of all the rules of inference that no formula disappears in a derivation. Thus, cut-free derivations have the subformula property: Each formula in the derivation of a sequent Γ ⇒ C is a subformula of this endsequent. Later we shall relax on this a bit, by letting atomic formulas disappear, and then the subformula property becomes the statement that each formula in a derivation is a subformula of the endsequent or an atomic formula. Such a weak subformula principle is still adequate for structural proof-analysis.

Standard applications of cut-elimination include elementary syntactic proofs of consistency, the disjunction property for intuitionistic systems, interpolation theorems, and so on. For the first, assume a system is inconsistent, i.e., assume that the sequent ⇒ ⊥ is derivable in it. But each logical rule adds a logical constant, and the axioms and weakening and contraction are rules that have formulas in the antecedent. Therefore there cannot be any derivation of ⇒ ⊥; a cut-free system is consistent. Similarly, assuming that ⇒ A ∨ B is derivable in a system of rules, it can be the case that the only way by which it can be concluded is by the rules for right disjunction. Thus, either ⇒ A or ⇒ B can be derived, and we say that the system of rules has the disjunction property. If a system is both cut-free and contraction-free, it can have the property that the premisses are proper parts of the conclusion, i.e., at least some formula is reduced to a subformula. In this case, we have a root-first proof search resulting in a tree that terminates. If the leaves of the tree thus reached are axioms, we can read it top-down as a derivation of the endsequent. But to show that a sequent is underivable, we have to be able to survey all possible derivations. For example assume that ⇒ P ∨ ∼ P is derivable in a cut-free intuitionistic system. Then the last rule is one of the two right disjunction rules, and either ⇒ P or ⇒ ∼P is derivable. But no logical rule concludes ⇒ P. If ⇒ ∼ P were derivable, the last rule would have had to be R⊃. Again, no logical rule concludes the premiss P ⇒ ⊥.

Above we found a way that led to the rules of sequent calculus from those of natural deduction. Often the structure of cut-free sequent calculus derivations is seen more clearly if it is translated back into natural deduction. This can be made algorithmic, as shown in Chapter 8. Not all sequent calculus derivations can be translated, but only those that do not have “useless” weakening or contraction steps. The translation is such that the order of application of logical rules is reflected in the natural deduction derivation. The meaning of a cut-free derivation is that all major premisses of elimination rules turn into assumptions.

The connection between sequent calculus and natural deduction is straightforward for single succedent sequent calculi, i.e., those with just one formula in the succedent to the right of the sequent arrow. But there are also systems with a whole multiset as succedent. It can be shown that systems of intuitionistic logic are obtained from classical multisuccedent systems by some innocent-looking restrictions on the succedents. In Chapter 5 we show that the converse is also true, at least for propositional logic: We obtain classical logic from intuitionistic single succedent sequent calculus by the addition of a suitable rule corresponding to the classical law of excluded middle.

Most of the research on sequent calculus has been on systems of pure logic. Considering that the original aim of proof theory was to show the consistency of mathematics, this is rather unfortunate. It is commonly believed that there is nothing to be done: That the main tool of structural proof theory, cut elimination, does not apply if mathematical axioms are added to the purely logical systems of derivation of sequent calculus. In Chapter 6 we show that these limitations can be overcome. A simple example of the failure of cut elimination in the presence of axioms is given by Girard (1987, p. 125): Let the axioms have the forms ⇒ A ⊃ B and ⇒ A. The sequent ⇒ B is derived from these axioms by

{⇒ A  {⇒ A ⊃ B {A ⇒ A B ⇒ B \atop A, A ⊃ B ⇒ B}^{L⊃} \atop A ⇒ B}_{Cut} \atop ⇒ B}_{Cut}

Inspection of sequent calculus rules shows that there is no cut-free derivation of ⇒ B, which leads Girard to conclude that “the Hauptsatz fails for systems with proper axioms” (ibid.). More generally stated, the cut elimination theorem does not apply to sequent calculus derivations with premisses.

We shall give a way of adding axioms to sequent calculus in the form of nonlogical rules of inference, and show that cut elimination need not be lost by such addition. This depends critically on formulating the rules of inference in a particular way. It then follows that the resulting systems of sequent calculus are both contraction- and cut-free. A limitation, not of the method, but one due to the nature of the matter, is that in constructive systems there will be some special forms of axioms, notably (P ⊃ Q) ⊃ R, that cannot be treated through cut-free rules. For classical systems, our method works uniformly. Gentzen’s original subformula property is lost, but typical consequences of that property, such as consistency, or the disjunction property for constructive systems, usually follow from the weaker subformula property.

To give an idea of the method, consider again the above example. With P and Q atomic formulas and C an arbitrary formula, P ⊃ Q is turned into a rule by stipulating that if Q ⇒ C, then P ⇒ C, and P is turned into a rule by stipulating that if P ⇒ C, then ⇒ C:

{Q ⇒ C \atop P ⇒ C}  {P ⇒ C \atop ⇒ C}

The sequent ⇒ Q now has the cut-free derivation

{Q ⇒ Q \atop P ⇒ Q} ; ⇒ Q

The method of converting axioms into cut-free systems of rules has many applications in mathematics, for example, it can be used in syntactic proofs of consistency and mutual independence for axiom systems. If we use classical logic, we can convert a theorem to be proved into a finite number of sequents that have no logical structure but only atomic formulas and falsity. By cut-elimination, their derivation uses only the nonlogical rules, and a very strong control on structure of derivations is achieved. In typical cases such as affine geometry, an axiom can be proved underivable from the rest of an axiom system by showing its underivability by the rules corresponding to these latter.

The aim of proof theory, as envisaged by Hilbert in 1904, was to give a consistency proof of arithmetic and analysis, and thereby to resolve the foundational problems of mathematics for good. There had been earlier consistency proofs, such as those for non-Euclidean geometries, in which a model was given for an axiom system. But such proofs are relative, they assume the consistency of the theory in which the model is given. Hilbert’s aim instead was an absolute consistency proof, carried through by elementary means. The results of Gödel in 1931 are usually taken to show such proofs an impossibility as soon as a system contains the principles of arithmetic. But we shall see in Chapter 6 that when this is not the case, purely syntactic and elementary consistency proofs can be obtained as corollaries to cut-elimination.

A whole branch of logical research is devoted to the study of intermediate logical systems. These are by definition systems that stand between intuitionistic and classical logic in deductive power. In Chapter 7, we shall study the structure of proofs in intermediate logical systems by presenting them as extensions of the basic intuitionistic calculus. One method of extension follows the model of extending this calculus by the rule of excluded middle. Such extension works perfectly for the logical system obeying the weak law of excluded middle, ∼ A∨ ∼∼ A. A limit is reached here, too, for in order to have a subformula property, the characteristic law of an intermediate logic is restricted to instances of the law with atomic formulas, as for the law of excluded middle. If the law for arbitrary formulas cannot be proved from the law for atoms, there is no good structural proof theory under this approach. Such is the case for Dummett logic, characterized by the law (A ⊃ B) ∨ (B ⊃ A). Another method that has been used, is to start with the multisuccedent intuitionistic calculus and to relax the intuitionistic restriction on the R⊃ rule. This approach will lead to a satisfactory system for Dummett logic.

Our approach to structural proof theory is mainly based on contractionand cut-free sequent calculi. But we also present, in Chapter 5, calculi in which weakening and contraction are explicit rules and only cut is eliminated. The sequent calculus rules of the previous section are precisely the propositional and structural rules of the first such calculus, in Section 5.1(a). Further, we also present a calculus in which there is no explicit weakening or contraction, but these are built into the logical rules. This calculus, studied in Section 5.2, can be described as a “sequent calculus in natural deduction style.” Sequent calculi with independent contexts are useful for relating derivations in sequent calculus to derivations in natural deduction. The use of special elimination rules in natural deduction brings problems that only vanish if the general elimination rules are taken into use. In Chapter 8 we show that this change will give an isomorphism between sequent calculus derivations and natural deduction derivations. The analysis of proofs via natural deduction can often provide insights it would be hard to obtain by the use of sequent calculus only.

Notes to Chapter 1:

The definition of languages through categorial grammars, and predicate logic especially, is treated at length in Ranta’s Type-Theoretical Grammar, 1994. A discussion of logical systems from the point of view of constructive type theory is given in Martin-Löf’s Intuitionistic Type Theory, 1984, but see also Ranta’s book for later developments.

An illuminating discussion of the nature of logical rules and the justification of introduction rules in terms of constructive meaning explanations is given in Martin-Löf (1985). Dummett’s views on these matters are collected in his Truth & Other Enigmas of 1979.

Our treatment of the elimination rules of natural deduction for propositional logic differs from the usual one that only recognizes the special elimination rules, as in Gentzen’s original paper “Untersuchungen über das logische Schliessen” (in two parts, 1934-35) or Prawitz’ influential book Natural Deduction: A Proof-Theoretical Study of 1965. The change is due to our formulation of the inversion principle in terms of arbitrary consequences of the direct grounds of the corresponding introduction rule, instead of just these direct grounds. The general elimination rule for conjunction is presented in Schroeder-Heister (1984). The reasons for the more general point of view will become clear in Chapter 8.

Natural deduction in sequent calculus style is used systematically in Dummett’s book Elements of Intuitionism of 1977.

Our way of obtaining classical propositional logic from the intuitionistic one uses the rule of excluded middle. It appears in this form, as a rule for arbitrary propositions, in Tennant (1978) and Ungar (1992), but the first one to propose the rule was Gentzen (1936). The rule has not been popular, for the obvious reason that it does not have the subformula property. Prawitz (1965) uses the rule of indirect proof and shows that its restriction to atomic formulas will give a satisfactory normal form and subformula property for derivations in the ∨-free fragment of classical propositional logic. We restrict in Chapter 8 the rule of excluded middle to atomic formulas and show that this gives a complete system of natural deduction rules and a full normal form for classical propositional logic. We also show that the rule can be restricted to atoms of the conclusion, thereby obtaining the full subformula property.

The long survey article by Prawitz, Ideas and results in proof theory, 1971, offers valuable insights into the development of structural proof theory. The notes to the chapters of Troelstra and Schwichtenberg’s Basic Proof Theory, 1996, also contain many historical comments.