Omitting types in Kripke models


Zoran Marković




When can a type be omitted in a Kripke model of some intu-itionistic theory is investigated. 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