From Commuting Conversions to Syntactic Identity
Gilda Ferreira (Universidade Aberta and CEMS UL)
Abstract: Commuting conversions are often regarded as the "price to pay'' for sequential syntax in natural deduction proofs or even as a sign of ``syntactic inadequacy''. This presentation explores translations of the Intuitionistic Propositional Calculus (IPC) into systems with no commuting conversions.
An example of such translations is the well-known Russell-Prawitz translation 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.
We will explore two different strategies for achieving proof identity preservation. The first strategy involves replacing System F with an atomic polymorphic target system. We will present and compare different versions of the Russell-Prawitz translation that follow this strategy [1,2,3]. The second strategy consists of introducing new atomization conversions to System F [4], obtaining not only proof identity preservation but also reduction preservation.
A recently developed translation [5], which completely avoids commuting conversions, shows that via the first strategy we can also achieve reduction preservation. Moreover, this new translation maps commuting conversions to syntactic identity, achieving a cleaner, ``commuting-conversion-free'' image of IPC.
This presentation includes significant joint work with José Espírito Santo.
1. F. Ferreira, G. Ferreira, Atomic polymorphism, The Journal of Symbolic Logic, 78(1), pp. 260-274, 2013.
2. P. Pistone, L. Tranchini, M. Petrolo, The naturality of natural deduction (II): On atomic polymorphism and generalized propositional connectives, Studia Logica, 110, pp. 545-592, 2022.
3. J. Espírito Santo, G. Ferreira, A refined interpretation of intuitionistic logic by means of atomic polymorphism, Studia Logica, 108, pp. 477-507, 2020.
4. 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.
5. J. Espírito Santo, G. Ferreira, How to avoid the commuting conversions of IPC, Theoretical Computer Science, 1033, 2025
logic
Audience: researchers in the topic
Series comments: Description: Seminar on all areas of logic
| Organizer: | Wesley Calvert* |
| *contact for this listing |