The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\) (Q720757)

The provability in a mathematical theory based on intuitionistic logic is an issue of particular interest not only technically but also philosophically, first of all from the viewpoint of constructivism. At the same time, however, it is also extremely complicated as has been suggested by several observations. For example, the disjunction property enjoyed in Heyting arithmetic HA is not formalizable in itself as shown by \textit{J. Myhill} [Proc. Am. Math. Soc. 39, 181--183 (1973; Zbl 0262.02026)] and \textit{H. Friedman} [Proc. Natl. Acad. Sci. USA 72, 2877--2878 (1975; Zbl 0342.02012)]. On the other hand, \textit{D. M. R. Leivant} [Absoluteness of intuitionistic logic. Amsterdam: Mathematisch Centrum. (1979; Zbl 0459.03024)] has shown that a slightly different certain schema for the HA-provability is available (while it is not valid with respect to the PA-provability, namely, that in the classical Peano arithmetic). As is well-known, \textit{R. M. Solovay} [Isr. J. Math. 25, 287--304 (1976; Zbl 0352.02019)] established the arithmetical completeness of propositional normal modal logic GL on PA, (that is, the PA-provability is formalized by the GL-modality for short), from which then the study of provability logic has been developed by Artemov, Visser, Beklemishev, and others. \par It is quite natural to consider the above problem in this framework by asking ``What is the provability logic of HA?'', which then is studied systematically by Visser, de Jongh, Iemhoff, and others. Nevertheless, the axiomatization of corresponding intuitionistic modal logic has not yet been established. \par In this paper, the authors give an answer to the question in the case of $\Sigma_1$-interpretations, that is, with respect to the validity by interpretations such that (propositional) variables are restricted to range over (arithmetical) $\Sigma_1$-sentences only. In the classical case, it is already examined by \textit{A. Visser} [Aspects of diagonalization and provability. Utrecht: Utrecht University (PhD Thesis) (1981)] that the restriction gives rise to the modal theory (not closed under formula substitution) obtained by extending GL with the completeness axiom for propositional variables (formalizing the so-called $\Sigma_1$-completeness in PA). \textit{A. Visser} [Ann. Pure Appl. Logic 114, No. 1--3, 227--271 (2002; Zbl 1009.03029)] has also investigated the intuitionistic case and set up an algorithm to determine for an arbitrarily given non-modal formula another satisfying certain syntactical characteristic (called NNIL-formula) under the condition that their HA-provabilities are equivalent in HA with any $\Sigma_1$-interpretation. This feature, say Visser's approximation for convenience, is generalized to all modal formulas in this paper by means of those called TNNIL-formula. The above mentioned Leivant principle [Leivant, loc. cit.] is also extended so as to be enjoyed by $\Sigma_1$-interpretations. Then the desired intuitionistic modal theory, denoted by $iH_\sigma$, is axiomatized, roughly saying, on the base of iGL (the intuitionistic version of GL) by the completeness axiom for propositional variables, the extended Leivant principle, and the axioms for the generalized Visser approximation. Thus, the axiomatization of $iH_\sigma$ itself is much more complicated than the usual. Moreover, the proof of its completeness, which is the central issue of this paper, is also carried out by several technically sophisticated lemmas to support. The kernel is of course the counter-model construction for a given modal formula not provable in $iH_\sigma$, namely, the existence of the $\Sigma_1$-interpretation to transform the modal formula into an arithmetic sentence not provable in HA. For this to do, the authors show that it can be done indeed if the given modal formula is a TNNIL-formula refuted by certain finite-tree Kripke model (for intuitionistic normal modal logic), where the method of Solovay is applied on such a Kripke model by making use of \textit{C. A. Smorynski}'s [``Applications of Kripke models'', Lect. Notes Math. 344, 324--391 (1973; \url{doi:10.1007/BFb0066744})] simulation to construct a Kripke model of HA from a propositional intuitionistic Kripke model. In addition, the intuitionistic normal modal logic iGLC (the extension of iGL by the schematic completeness axiom) is proved to be characterizable by the class of such finite-tree Kripke models as required. Then, another key observation is that $iH_\sigma$ and iGLC are proved to agree on TNNIL-formulas, from which then follows the completeness of $iH_\sigma$ according to the generalized Visser's approximation. This completeness proof (as well as the deterministic feature of axiomatization) establishes the decidability of $iH_\sigma$ as an immediate consequence. Moreover, it is also shown as a by-product that the extension of HA by the formalized inconsistency statement enjoys the de Jongh property.