ABSTRACT
The theorem that claims the admissibility (or rather, eliminability) of the single cut rule for LK and LJ was termed Hauptsatz by Gentzen. “Hauptsatz” simply means main theorem in German. However, in the English language literature, the term is used exclusively for the cut theorem. (Surely, there are other important or main theorems out there!) The cut rule is vital for any sequent calculus as we explain in detail in Section 7.8. It is much preferable to have the cut rule as an admissible rule rather than an explicit rule, because of the benefits of having the cut rule available when needed without always having to deal with it. Thus the Hauptsatz is indeed important.
