RELATIVE UNIFICATION IN INTUITIONISTIC LOGIC: TOWARDS THE PROVABILITY LOGIC OF HA

Abstract This article studies relative unification and admissibility in intuitionistic logic. We generalize results of [3, 7] and prove them relative to ${\mathsf {N}}$ formulae, the class of forlmulae with No Nested Implications to the Left. The main application of this generalization is to characterize the provability logic of Heyting Arithmetic $\mathsf {HA}$ and prove its decidability [16].