BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Gilda Ferreira (Universidade Aberta and CEMS UL) DTSTART:20260115T190000Z DTEND:20260115T200000Z DTSTAMP:20260423T035736Z UID:OLS/190 DESCRIPTION:Title: Fr om Commuting Conversions to Syntactic Identity\nby Gilda Ferreira (Uni versidade Aberta and CEMS UL) as part of Online logic seminar\n\n\nAbstrac t\nCommuting conversions are often regarded as the "price to pay'' for seq uential syntax in natural deduction proofs or even as a sign of ``syntacti c inadequacy''. This presentation explores translations of the Intuitionis tic Propositional Calculus (IPC) into systems with no commuting conversion s.\n\nAn example of such translations is the well-known Russell-Prawitz tr anslation which maps IPC into a highly expressive system known as System F \, or polymorphic lambda calculus. Despite the elegance of this embedding\ , it fails to preserve proof reduction or even proof identity.\n\nWe will explore two different strategies for achieving proof identity preservation . The first strategy involves replacing System F with an atomic polymorphi c target system. We will present and compare different versions of the Rus sell-Prawitz translation that follow this strategy [1\,2\,3]. The second s trategy consists of introducing new atomization conversions to System F [4 ]\, obtaining not only proof identity preservation but also reduction pres ervation.\n\nA recently developed translation [5]\, which completely avoid s commuting conversions\, shows that via the first strategy we can also ac hieve reduction preservation. Moreover\, this new translation maps commuti ng conversions to syntactic identity\, achieving a cleaner\, ``commuting-c onversion-free'' image of IPC.\n\nThis presentation includes significant j oint work with José Espírito Santo.\n\n1. F. Ferreira\, G. Ferreira\, At omic polymorphism\, The Journal of Symbolic Logic\, 78(1)\, pp. 260-274\, 2013.\n\n2. P. Pistone\, L. Tranchini\, M. Petrolo\, The naturality of nat ural deduction (II): On atomic polymorphism and generalized propositional connectives\, Studia Logica\, 110\, pp. 545-592\, 2022.\n\n3. J. Espírito Santo\, G. Ferreira\, A refined interpretation of intuitionistic logic by means of atomic polymorphism\, Studia Logica\, 108\, pp. 477-507\, 2020.\ n\n4. J. Espírito Santo\, G. Ferreira\, The Russell-Prawitz embedding and the atomization of universal instantiation\, Logic Journal of the IGPL\, 29(5)\, pp. 823-858\, 2021.\n\n5. J. Espírito Santo\, G. Ferreira\, How t o avoid the commuting conversions of IPC\, Theoretical Computer Science\, 1033\, 2025\n LOCATION:https://researchseminars.org/talk/OLS/190/ END:VEVENT END:VCALENDAR