History of Logic Seminar Series - Talk: E. Moriconi, "Remarks on Sequent Calculus" (20.05.2026)
antpic...@gmail.com
We are pleased to announce the ninth session of the second annual cycle of the History of Logic Seminar Series. The session will be held on Wednesday, May 20, from 3 to 5 p.m. CEST.
To have the Zoom link, please subscribe to the HoL Mailing List by contacting us at the link provided below.
On this occasion, we will host a talk by Enrico Moriconi (University of Pisa). His talk is titled Remarks on Sequent Calculus. Here is a short abstract:
In the last section V of his thesis, after the proof of the Hauptsatz, Gentzen proved the equivalence between the main three types of formalization of the logical inference: the Hilbert-Ackermann system (H.A.), the Natural Deduction Calculus (N.D.), and the Sequent Calculus (S.C.). In this proof we can see, so to say, the birth of the same formalism of S.C., which is maybe the most important formalization of logical deduction ever provided. Also the handwritten version of the thesis, let’s say Ms.ULS, contains a similar proof of equivalence, as we have learnt from the important researches made by Jan von Plato on the newly found Gentzen’s texts. Admittedly, the last section of the thesis is normally rated “less important” than the other sections, but nonetheless it casts some important light on the emergence of the S.C., and more generally on some structural features of Gentzen’s work. In the Thesis the equivalence proof proceeds through the following sequence of steps: i) a proof that every derivation within the H.A.-axiomatization can be transformed in an equivalent derivation of N.D.-calculus; ii) a proof that every N.D.-derivation can be transformed into an equivalent S.C.-derivation; iii) a proof that every S.C.-derivation can be transformed into an equivalent H.A.-derivation. The proof is conducted first for Intuitionistic logic and afterward for Classical logic. In this way, of course, the goal to prove the equivalence of all three calculi is accomplished. However, the main single component showing the origin of S.C. is the translation of derivations built within N.D.-formalism into derivations built within the axiomatic logical calculus of Hilbert and Ackermann’s book. And it is interesting to note that in the pertinent part of Ms.ULS Gentzen provided a proof of the equivalence between N.D.-calculi and the H.A.-formalism by showing the possibility to translate every (classical) N.D.-derivation into an equivalent H.A.-derivation; in this way it is explicitly supplied a missing link which is only implicitly present, as a by-product of previous steps i)-iii), in the published version of the thesis.
For more information, please visit our website. Feel free to share the news and invite other scholars to subscribe to this mailing list, and do not hesitate to contact historyofl...@gmail.com with any questions you might have.
Kind regards,
Francesco, Antonio, and Francesco