×

zbMATH — the first resource for mathematics

Omitting types in Kripke models. (English) Zbl 0843.03021
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)
PDF BibTeX XML Cite