A study of Normalization in Classical Logic

This is my thesis for the Master’s degree in Philosophy.

Abstract

This master’s thesis (in Italian) explores various normalization procedures (also known as cut-elimination procedures, from Gentzen’s original work on the subject [4]) in sequent-style deductive systems for classical logic. In the 4^th and main chapter of the thesis I adapt a proof technique by Barbanera and Berardi [2] to obtain a strong normalization result for a variant of Gentzen’s non-deterministic cut-elimination procedure for the sequent calculus LK, as defined in [3,1]. This opens the door to a direct investigation of the computational content of symmetric reduction procedures for classical sequent calculus.

Note: it turned out that the same result had already been published by Urban and Bierman in [5], a paper I had missed during my survey of relevant literature. Although my work is similar to theirs even in very small details, it was an independent rediscovery, and in fact some technical choices helped me avoid a (non-critical) mistake that was present in [5].

References

[1] Abrusci, V.M., and Tortora de Falco, L. Logica: Volume 1 — Dimostrazioni e modelli al primo ordine. Springer Milan (2014)
[2] Barbanera, F., and Berardi, S. «A symmetric λ-calculus for classical program extraction». In: Information and Computation 125(2), 103—117 (1996)
[3] Danos, V., Joinet, J.-B., and Schellinx, H. «A New Deconstructive Logic: Linear Logic». In: The Journal of Symbolic Logic 62(3), 755—807 (1997)
[4] Gentzen, G. «Untersuchungen über das logische Schließen. I». In: Mathematische Zeitschrift 39(1), 176—210 (1935)
[5] Urban, C., and Bierman, G. M. «Strong Normalisation of Cut-Elimination in Classical Logic». In: Girard, J.-Y. (ed.) Typed Lambda Calculi and Applications, pp. 365—380. Springer Berlin Heidelberg (1999)