×

Extensions of Kripke models. (English) Zbl 1492.03004

Summary: There are several ways to define the notion of submodel for Kripke models of intuitionistic first-order logic. In our approach, a Kripke model \(\mathfrak{A}\) is a submodel of a Kripke model \(\mathfrak{B}\) if the frame of \(\mathfrak{A}\) is a subframe of the frame of \(\mathfrak{B}\) and for each two corresponding worlds \(A_\alpha\) and \(B_\alpha\) of them, \(A_\alpha\) is a classical submodel of \(B_\alpha\). In this case, \(\mathfrak{B}\) is called an extension of \(\mathfrak{A}\). We characterize formulas that are preserved under taking extensions of Kripke models.

MSC:

03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: DOI