The greatest extension of S4 into which intuitionistic logic is embeddable (Q1378428)

The main result of the paper is the existence of the greatest quasi-normal `modal companion' of the intuitionistic logic Int, i.e. the existence of the greatest extension \(M^\ast\) of S4 into which Int is embeddable by Gödel translation (a quasi-normal modal logic is closed under substitution and modus ponens, but not necessarily under \(\square\)-introduction). This is an analogue of the well-known fact that Grzegorczyk logic Grz is the greatest normal modal companion of Int. The logic \(M^\ast\) is explicitly axiomatized by an infinite set of axioms; the question of its finite axiomatizability remains open. Also it is proved that \(M^\ast\) is decidable, lacks the fmp (and thus is a proper extension of Grz), is Halldén-complete and has the modal disjunction property. On the other hand, the analogue of the Blok-Esakia theorem for \(M^\ast\) fails: the author constructs an intermediate logic which has no modal companions among the extensions of \(M^\ast\). The proofs are based on the method of canonical formulas developed by the author in many papers.