Provability logic and the completeness principle (Q1740459)

Provabiltiy logic is a modal description of provability predicate of sufficiently strong arithmetical theory. Any \(\Sigma_1\)-sound theory interpreting \textsf{EA} (elementary arithmetic) has the same provability logic as \textsf{EA}: Gödel-Löb logic \textsf{GL}. It is unknown what the provability logic of \textsf{HA} (Hayting arithmetic) exactly is. An intuitionistic version of \textsf{GL} is denoted by \textsf{iGLC} and it consists \textsf{GL}, plus the Completeness principle \(\Box p\rightarrow p.\) The main goal of the article is to find interesting situations where we can give a Solovay-style embedding of a model for the logic \textsf{iGLC}. The authors presented their Solovay-style embedding in detail. Arithmetical completeness for \textsf{iGLC} in various theories and for various interpretations of modal operator \(\Box\) is obtained. As a corollary, \(\Sigma\)-provability of \textsf{HA} is determined. \textit{M. Ardeshir} and \textit{M. Mojtahedi} [Ann. Pure Appl. Logic 169, No. 10, 997--1043 (2018; Zbl 1426.03039)]. But they use different methods.