A proof of Gentzen's \textit{Hauptsatz} without multicut (Q5928308)

The celebrated Gentzen's cut elimination theorem does not really eliminate cuts themselves, but multicuts (Mischung). The reason is the following. If one eliminates cuts one at a time, the case when the cut formula is the result of contraction causes difficulty, because ranks of cuts may increase, and so the inductive procedure does not work. In this paper, the author overcomes this difficulty by using the familiar inversibility result. The case when the cut formula is \(A\& B\) and the logic is intuitionistic is the clearest for seeing the point. If \(\Gamma\to A\& B\) is derivable, then certainly \(\Gamma\to A\) and \(\Gamma\to B\) are. Also when \(A\& B\), \(\Gamma\to \Delta\) is derived without cut, its proof can be inverted to that of \(A,B,\Gamma \to\Delta\), even if \(A\& B\) was the principal formula of contraction. So, instead of cutting \(A\& B\), one can cut the simpler formulas \(A\) and \(B\). And these cuts are eliminable according to the induction hypothesis. For the cases of other connectives and quantifiers, and of classical logic, the formulations take more complex forms, but the idea is the same.