Omitting types in Kripke models. (English) Zbl 0843.03021

Marković, Zoran

Filomat 9, No. 3, 803-807 (1995).

Summary: We investigate when a type can be omitted in a Kripke model of some intuitionistic theory. As it is usual with intuitionistic systems, various classically equivalent formulations of the Omitting Types Theorem become nonequivalent statements in the intuitionistic setting. Several such formulations are discussed in terms of whether they have the intended meaning in Kripke models, and several theorems are proved.

MSC:

03C90	Nonclassical models (Boolean-valued, sheaf, etc.)
03B20	Subsystems of classical logic (including intuitionistic logic)

Keywords:

intuitionistic logic; omitting types theorem; Kripke model