The embedding theorem: its further developments and consequences. I (Q2372685)

The embedding of intuitionistic logic into the modal logic S4 by the so-called Gödel-McKinsey-Tarski translation and its generalizations by Grzegorczyk, Maksimova, et al. provide useful means for a comparative study between lattices of intermediate logics (ExtInt) and of normal modal extensions of S4 (ExtS4). After surveying the development of the study, the author shows in this paper several results on structural aspects of these lattices. In particular, it is pointed out that ExtInt is likely to be the only constructing block with which ExtS4 can be formed. The paper includes many interesting problems and conjectures to suggest further developments of the study in this direction, and will be continued in Part II where the embedding theorem is analyzed algebraically.