Classical Sequents
In this section we offer a concise introduction to the sequent calculus, a well- known and powerful tool in structural proof theory and applications. Out of a large variety of formats for sequent calculi we opted for one that provides a compact and yet rigorous path to classical logic, and subsequently to S4, and which plays a pivotal role in this area.
From time to time we will mention where our formal choices could have been different. Ultimately, these differences make no difference.
Definition 5.1 A sequent is an ordered pair of finite sets of formulas Γ, A, traditionally written as
Here Γ is called the antecedent and A the succedent of the sequent.
We note that in alternate formulations, Γ and A are sometimes taken to be finite multisets, or even finite sequences of formulas.
sumptions Γ. In such reading, A is understood to be the disjunction of all its formulas. This intuition is formalized in the following definition.
Definition 5.2 By the formula translation of a sequent
we mean
formula
Definition 5.3 [Classical Sequent Calculus] We now define a sequent calculus Gcl with the following axioms and rules of inference. 
Cut:
We note that in some formulations Weakening is not a rule, but rather the effect is built into the axioms.
For instance,
The two versions are easily seen to be equivalent.
The reader is probably aware of the term “cut-elimination” reflecting the desire to look for derivations that do not involve the Cut rule. What is wrong with the Cut and why should we try to avoid it? After all, the Cut appears to be a sequent counterpart of the syllogism logic rule
The Cut rule is the only rule in Gcl that violates the so-called subformula property: every formula occurring in the premise sequents of a rule is a subformula in the conclusion sequent. Consequently, a cut-free derivation of a sequent
contains only subformulas of Γ, A. Because this is a finite set, it makes it theoretically possible to do a bottom-up proof search, which forms the basis for semantic tableaus. Conceptually, in cut-free derivations, the aggregated complexity of formulas grows from premises to conclusions. (We note that some derivation steps could be void, i.e., do not change sequents.) This allows for the valuable possibility of complexity-based induction along derivation trees.
Perhaps, the easiest consequence of cut-freeness begins with the observation that the empty sequent cannot not have a cut-free derivation (which is immediate from the subformula property). On the other hand, an inconsis-
Conclusion: cut-free derivation systems are consistent, and in the areas of proof theory that study consistency questions, proving a cut-elimination theorem is a valuable tool for establishing consistency.
In the justification logic project, cut-free derivations were used in the early proofs of the Realization Theorem, cf. Chapter 6.
Example 5.4 Here is a proof in
We have combined multiple applications of Weakening into one abbreviated version called W, for simplicity.
For brevity, unless the opposite is explicitly mentioned, we consider the language with Boolean connectives → and ? and regard other connectives ë, v, : as definable.
Theorem 5.5 (Atomic Axiomatization) Each theorem of Gcl- can be derived in Gcl- with atomic axioms only 
where p is any propositional letter.
5.3