Speaker: René Gazzari, CMAT

Date: Thursday, 23 March 2023, 14h30

Venue: Room B4009 (sala de seminários do DMAT)

Abstract:

Gentzen [2] introduced in his seminal paper “Introduction into Logical Deduction” the calculus of Natural Deduction. His intention was to provide a formal representation of proofs as close as possible to real mathematical praxis.

In our opinion, he succeeded with respect to the representation of argumentations with statements. But unfortunately, mathematicians not only argue (with statements), but occasionally they also calculate (with objects like numbers and sets) in their proofs. As the standard representation of such calculations (via proofs dealing with equations) seems quite artificial, we proposed the calculus of Natural Calculation [1], an extension of Natural Deduction by term rules permitting a natural representation of such calculations in proofs.

In our talk, we provide an introduction into this extension of Natural Deduction and discuss its basic proof-theoretic properties. Central result, besides soundness and completeness, is that every (formal) calculation can be transformed into a linear calculation. If time permits, we will address some more advanced topics related to the calculus of Natural Calculation.

References
[1] R. Gazzari. The Calculus of Natural Calculation. Studia Logica, 109:1375–1411, 2021.
[2] G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor,The Collected Papers of Gerhard Gentzen, Studies in Logic and the Foundations of Mathematics, pages 68–131. North-Holland, Amsterdam, 1969.