On the theory of models for intuitionistic logic

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.
Bibliography: 14 titles.