On the theory of models for intuitionistic logic. (English. Russian original) Zbl 0568.03018

Math. USSR, Sb. 48, 223-235 (1984); translation from Mat. Sb., Nov. Ser. 120(162), No. 2, 227-239 (1983).
A model approach is developed for intuitionistic and classical theories in the language of the simple theory of types. A weak form of completeness theorem is proved, of which the Henkin completeness theorem is a special case. An ultraproduct of Kripke structures is introduced, and an application of the omitting types theorem to theories with infinite rules for deduction is given.


03C95 Abstract model theory
03F55 Intuitionistic mathematics
03C20 Ultraproducts and related constructions
03C35 Categoricity and completeness of theories
03B15 Higher-order logic; type theory (MSC2010)
03B55 Intermediate logics
Full Text: DOI