Relative Unification in Intuitionistic Logic: Towards provability logic of HA

TL;DR

The paper advances a relativized approach to unification, admissibility, and preservativity in intuitionistic logic by extending Ghilardi’s and Iemhoff’s frameworks to NNIL({par}) formulas. It develops a detailed construction of relative projectivity and extendibility, yields finitary projective resolutions, and provides a complete AR-based calculus (AR$_{\sf par}$ and AR$^{+}_{\sf par}$) for ${\sf N}$-admissibility and ${\downarrow}^{\!^{}}{\sf N}$-preservativity. These results culminate in a characterization and decidability result for the provability logic of Heyting Arithmetic $HA$, situating the PLHA problem within a concrete, computable framework. Overall, the work supplies explicit, algorithmic tools for analyzing derivability, admissibility, and preservativity in intuitionistic settings, with direct implications for provability logic and related conservativity questions in constructive arithmetic.

Abstract

This paper studies relative unification and admissibility in the intuitionistic logic. We generalize results of [Ghilardi, 1999; Iemhoff, 2001a] and prove them relative in NNIL(par) propositions, the class of propositions with No Nested Implications in the Left made up from parameters. The main application of such generalization is to characterize provability logic of Heyting Arithmetic HA and prove its decidability [Mojtahedi, 2022].

Figures (1)

• Figure 1: List of symbols and notations

Theorems & Definitions (136)

• Theorem 2.1
• proof
• Theorem 2.2
• proof
• Theorem 2.3: Soundness
• proof
• Theorem 2.4
• proof
• Theorem 2.5
• proof