[NOVA Math] Seminar of Algebra and Logic

The Center of Mathematics and Applications (NOVA Math), promote the Seminar of Algebra and Logic with the title: “Translations between logics: a unified view”. Gilda Ferreira (Universidade Aberta and CEMS.UL/CMAFcIO) is the speaker.

Abstract: We begin with a very introductory overview of classical, intuitionistic, and linear logics. Several proof translations exist between classical and intuitionistic logic (negative translations) [1, 2, 3], as well as between intuitionistic and linear logic (Girard translations) [4, 5]. These translations serve various purposes, including transferring properties between systems, simplifying proofs, facilitating the extraction of constructive computational content from proofs, and controlling the use of logical resources.

      We will show that all these systems can be expressed as extensions of a basic logical system (essentially, intuitionistic linear logic).

      By establishing a common logical basis, we are able to formalize a unified approach to devising and simplifying such proof translations [6]. This approach clarifies the relationships between different logical systems, and reveals the underlying structure that connects them. Through this simplification process, we obtain the most well-known translations in the literature.

      This is joint work with Paulo Oliva and Clarence Protin.

References

[1] A.S. Troelstra, D. van Dalen, Constructivism in mathematics: An introduction. In Studies in Logic and the Foundations of Mathematics, volume

     1, 1988.

[2] M. Heine Sørensen, P. Urzyczyn, Lectures on the Curry-Howard Isomorphism, volume 149. Elsevier, 2006.

[3] G. Ferreira, P. Oliva, On various negative translations, Electronic Proceedings in Theoretical Computer Science, 47:21-33, 2011.

[4] J.-Y. Girard, Linear logic, Theoretical Computer Science, 50:1–101, 1987.
[5] J.-Y. Girard, A tutorial on linear logic. In Substructural Logics, Studies in Logic and Computation 2, pages 327–355. Oxford Science Publications,
     1994.

[6] G. Ferreira, P. Oliva, C. Protin, On the various translations between classical, intuitionistic and linear logic. (subm.)

     https://arxiv.org/abs/2409.02249

 Monday, 10 February 2025, at 14:00.