How to avoid the commuting conversions of IPC

TL;DR

The paper tackles the problem of embedding $IPC$ into the predicative fragment $F_{at}$ of System $F$, where previous embeddings fail to preserve commuting conversions. It introduces an optimized translation denoted $(\cdot)^{\lozenge}$ that uses Russell-Prawitz formula translations and novel optimized eliminators to map commuting conversions to syntactic identity while preserving $\beta\eta$-reductions. The authors prove a simulation theorem establishing that reductions in $IPC$ are faithfully simulated in ${F}_{at}$ under this embedding, effectively yielding a commuting-conversion-free image of $IPC$ in ${F}_{at}$. They also address special cases (notably $\pi_{\supset}$) and discuss the scope, limitations, and potential implications for faithful encodings of propositional intuitionistic logic into predicative second-order frameworks.

Abstract

Since the observation in 2006 that it is possible to embed IPC into the atomic polymorphic lambda-calculus (a predicative fragment of system F with universal instantiations restricted to atomic formulas) different such embeddings appeared in the literature. All of them comprise the Russell-Prawitz translation of formulas, but have different strategies for the translation of proofs. Although these embeddings preserve proof identity, all fail in delivering preservation of reduction steps. In fact, they translate the commuting conversions of IPC to beta-equality, or to other kinds of reduction or equality generated by new principles added to system F. The cause for this is the generation of redexes by the translation itself. In this paper, we present an embedding of IPC into atomic system F, still based on the same translation of formulas, but which maps commuting conversions to syntactic identity, while simulating the other kinds of reduction steps present in IPC betaη-reduction. In this sense the translation achieves a truly commuting conversion-free image of IPC in atomic system F.

Figures (7)

• Figure 1: The main result of the present paper in context. Simulation of a commuting conversion $M\to_R N$ in $\mathbf{IPC}$. System $\mathbf{F}$ to the right of dashed line. System ${\mathbf{F}}_{\mathbf{at}}$ between the dashed and dotted lines. Comparison of map $(\cdot)^{\star}$ (proposed in FerreiraFerreira2009FerreiraFerreira2013), map $(\cdot)^{\circ}$ (proposed in EspiritoSantoFerreira2020), map $(\cdot)^{\bullet}$ (proposed in EspiritoSantoFerreira2021), and map $(\cdot)^{\lozenge}$ (proposed here). Some reductions are "administrative", as argued in EspiritoSantoFerreira2020. The reductions $N^{\star}\to^*Q$ and $N^{\circ}\to^* Q$ go in the wrong direction, causing $M\to N$ to be mapped to the $\beta$-equalities $M^{\star}=_{\beta}N^{\star}$ and $M^{\circ}=_{\beta}N^{\circ}$. The map $(\cdot)^{\bullet}$ simulates $M\to N$ with the help of atomization reductions $\rho\varrho$ added to $\mathbf{F}$ in EspiritoSantoFerreira2021. The map proposed here makes the commuting conversion $M\to N$ disappear: $M^{\lozenge}=N^{\lozenge}$.
• Figure 2: Typing/inference rules
• Figure 3: Reduction rules of $\mathbf{IPC}$
• Figure 4: Optimized elimination constructions
• Figure 5: The optimized translation of proof terms

Theorems & Definitions (70)

• Definition 1
• Definition 2
• Definition 3
• Definition 4: Optimized translation
• Lemma 1
• proof
• Proposition 1
• proof
• Lemma 2
• proof