Atomization alternatives in the RussellPrawitz translation
Gilda Ferreira^{1}
^{1} University of Lisbon
In this presentation, we explore various versions of the RussellPrawitz translation, which maps intuitionistic propositional calculus to secondorder propositional logic. The target system, introduced independently by JeanYves Girard and John Reynolds, is known as System F or polymorphic lambdacalculus. 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.