ABSTRACT
The first sequent calculus, LK is the example after which many other calculi have been fashioned. We describe this calculus, prove its equivalence to the axiom system K, and provide a sound and complete interpretation too. A major part of this chapter presents the proof of the cut theorem using triple induction. We avoid the detour via the mix rule by using a suitable formulation of the single cut rule, and by adding a new parameter to the original double induction. Although we do not go through all the details of this proof, we hope that sufficient details are included so that the structure of the proof becomes completely clear. Later on, we will provide more condensed proofs of cut theorems or simply state cut theorems with reference to this proof.
