Substitutions of Σ⁰₁-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic

This paper is concerned with notions of consequence. On the one hand, we study admissible consequence, specifically for substitutions of Σ⁰₁-sentences over Heyting arithmetic (HA). On the other hand, we study preservativity relations. The notion of preservativity of sentences over a given theory is a dual of the notion of conservativity of formulas over a given theory. We show that admissible consequence for Σ⁰₁-substitutions over HA coincides with NNIL-preservativity over intuitionistic propositional logic (IPC). Here NNIL is the class of propositional formulas with no nestings of implications to the left. The identical embedding of IPC-derivability (considered as a preorder and, thus, as a category) into a consequence relation (considered as a preorder) has in many cases a left adjoint. The main tool of the present paper will be an algorithm to compute this left adjoint in the case of NNIL-preservativity. In the last section, we employ the methods developed in the paper to give a characterization the closed fragment of the provability logic of HA.