×

From forcing to satisfaction in Kripke models of intuitionistic predicate logic. (English) Zbl 1492.03003

Summary: In this paper, we answer a natural question concerning the relation between forcing and satisfaction in Kripke models of intuitionistic predicate logic. We define a class of formulas denoted by \(\mathsf{R}^*\), with the property that forcing of any \(\mathsf{R}^*\)-formula in a node of a Kripke model of intuitionistic predicate logic implies its satisfaction in the classical structure attached to that node. We also prove that any formula with this property is an \(\mathsf{R}^*\)-formula.

MSC:

03B20 Subsystems of classical logic (including intuitionistic logic)
03C25 Model-theoretic forcing
Full Text: DOI