A refined interpretation of intuitionistic logic by means of atomic polymorphism (Q2186692)

The atomic system \(F_{at}\) is a fragment of Girard's system \(F\) induced by restricting to atomic instances the elimination inference rule for \(\forall\) and the corresponding proof term constructor. The authors study an embedding of intuitionistic propositional calculus IPC formulated as a system with proof terms into \(F_{at}\) alternative to the so-called canonical embedding proposed by \textit{F. Ferreira} [J. Philos. Log. 35, No. 1, 1--8 (2006; Zbl 1101.03014)]. The proposed translation of proofs is based, not on instantiation overflow, but instead on the admissibility of the elimination rules for disjunction and absurdity (where these connectives are defined according to the Russell-Prawitz translation). As compared to the embedding based on instantiation overflow, the alternative embedding works equally well at the levels of provability and preservation of proof identity, but it produces shorter derivations and shorter simulations of reduction sequences. Lambda-terms are employed in the technical development so that the algorithmic content is made explicit, both for the alternative and the original embeddings.