Kripke-style models for typed lambda calculus (Q804559): Difference between revisions

As an extension for usual Henkin models, Kripke-style models are defined for typed lambda calculus. As for the relationship between the models and Cartesian closed categories (CCCs), every Kripke model determines a CCC, and every small CCC may be embedded in a Kripke model. Kripke models are Cartesian closed subcategories of the presheaves over a poset. Strong completeness is proved for Kripke models: every set of equations that is closed under implication is the theory of a single Kripke model. Moreover, the notion of logical relations over Kripke structures is developed, showing that every theory is the theory of a model determined by a Kripke equivalence relation over a Henkin model.