Atomization alternatives in the Russell-Prawitz translation
Gilda Ferreira1
1 University of Lisbon
In this presentation, we explore various versions of the Russell-Prawitz translation, which maps intuitionistic propositional calculus to second-order propositional logic. The target system, introduced independently by Jean-Yves Girard and John Reynolds, is known as System F or polymorphic lambda-calculus. We analyze some properties of System F and the translation, with a focus on atomic polymorphism and atomization conversions. Our investigation examines the impact of introducing new atomization conversions to System F [2] and the more radical option of replacing System F with an atomic polymorphic target system. Specifically, we cover:
-
The original atomic polymorphic variant based on instantiation overflow [4][5].
-
Enhancements such as a variant that improves proof and reduction sequence sizes through an improved form of instantiation overflow [6].
-
A variant based on the admissibility of disjunction and absurdity elimination rules, resulting in more compact proves and reduced administrative reductions [1].
-
An approach that produces an image of intuitionistic propositional calculus truly free from commuting conversions [3].
This exploration includes significant joint work with José Espírito Santo.
References
[4] F. Ferreira, Comments on predicative logic, Journal of Philosophical Logic, 35, pp. 1–8, 2006.