L'Hauptsatz di Gentzen

[Autom. eng. transl.] The text analytically exposes the proof of the Cut elimination theorem (Hauptsatz) demonstrated by G. Gentzen in his "Untersuchungen über das logische Schliessen," Mathematische Zeitschrift 39 (1935), pp. 176-210, pp. 405-431, English translation in ME Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam-London, Investigations into Logical Deduction, 1969, pp. 68-131. The original demonstration by Gentzen is a demonstration based on a double induction, on the rank of the derivations and on the degree of the formula subject to the cut. In this text the demonstration is a double induction demonstration, but on the length of the derivation and on the degree of the formula subject to the cut. The method we followed is resumed with improvements in the formal rigor and analytical completeness of the passages from L. Heindorf, Elementary Beweistheorie, Wissenschaftsverlag, Mannheim 1994, pp. 103-140. Furthermore, there are two differences. First, while Heindorf demonstrates the theorem for intuitionistic calculus LJ, we prove it by the classical LK calculation. Secondly, our calculation contains only the structural rule of Weakening and this allows to simplify the proof of the cut elimination theorem, avoiding having to resort to the fusion rule equivalent to that of the cut. A similar method is also followed by R. David, K. Nour, C. Raffalli, Introduction à la logique. Théorie de la démonstration, Dunod, Paris 2003, pp. 200-211. Also other expositions of the theorem differ from the original proof. See, for example, the demonstration sketched in JY Girard, Prooftheory and Logical Complexity, vol. I, Bibliopolis, Naples, pp. 105-114, based on the double induction on the height of the derivation (height) and on the degree of complexity (degree) of the formula subject to the cut. For other methods see chap. 4 by AS Troelstra, H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, 2000, pp. 92-146. A general text on the various Cut-elimination methods is M. Baaz, A. Leitsch, Methods of Cut-Elimination, Springer, Dordrecht-NewYork 2011. Recently a unique issue of Studia Logica was published concerning the deduction systems invented by Gentzen and by Jaskowski and perfected by other scholars. It is a Special Issue by Andrzej Indrzejczak, "Gentzen's and Jaskowski's Heritage. 80 Years of Natural Deduction and Sequent Calculi ", Studia Logica (2014), 102. The volume is divided into three parts: the first includes a preliminary presentation of the LK sequent calculation. The second states and demonstrates the Hauptsatz. In the third, some important consequences of the Hauptsatz are illustrated, some of a formal nature, others of a more philosophical meaning. The second part is enriched with a technical appendix.