The Russell-Prawitz embedding and the atomization of universal instantiation

TL;DR

This paper introduces new conversions in system F to enforce atomic universal instantiation, improving proof simulation and connecting different translations of intuitionistic propositional logic.

Contribution

It presents novel atomization conversions in system F that enhance proof simulation and clarify the relationship between various embeddings of IPC.

Findings

Enforce atomic universal instantiation in system F

Enable strict proof reduction simulation via Russell-Prawitz embedding

Bridge between Russell-Prawitz embedding and other IPC translations

Abstract

Given the recent interest in the fragment of system F where universal instantiation is restricted to atomic formulas, a fragment nowadays named system F_at, we study directly in system F new conversions whose purpose is to enforce that restriction. We show some benefits of these new atomization conversions: (1) They help achieving strict simulation of proof reduction by means of the Russell-Prawitz embedding of IPC into system F; (2) They are not stronger than a certain "dinaturality" conversion known to generate a consistent equality of proofs; (3) They provide the bridge between the Russell-Prawitz embedding and another translation, due to the authors, of IPC directly into system F_at; (4) They give means for explaining why the Russell-Prawitz translation achieves strict simulation whereas the translation into F_at does not.