Relative Unification in Intuitionistic Logic: Towards provability logic of HA

TL;DR

This paper extends the understanding of relative unification and admissibility in intuitionistic logic, specifically focusing on NNIL propositions, to characterize the provability logic of Heyting Arithmetic and establish its decidability.

Contribution

It generalizes previous results to NNIL propositions and applies these to characterize and prove the decidability of the provability logic of HA.

Findings

Generalized unification results to NNIL propositions

Characterized provability logic of HA

Proved decidability of the provability logic

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].