×

Syntactic preservation theorems for intuitionistic predicate logic. (English) Zbl 1254.03016

Summary: We define notions of homomorphism, submodel, and sandwich of Kripke models, and we define two syntactic operators analogous to universal and existential closure. Then we prove an intuitionistic analogue of the generalized (dual of the) Lyndon-Łoś-Tarski theorem, which characterizes the sentences preserved under inverse images of homomorphisms of Kripke models, an intuitionistic analogue of the generalized Łoś-Tarski theorem, which characterizes the sentences preserved under submodels of Kripke models, and an intuitionistic analogue of the generalized Keisler sandwich theorem, which characterizes the sentences preserved under sandwiches of Kripke models. We also define several intuitionistic formula hierarchies analogous to the classical formula hierarchies \(\forall_n (= \Pi^0_n)\) and \(\exists_n (=\Sigma^0_n)\), and we show how our generalized syntactic preservation theorems specialize to these hierarchies. Each of these theorems implies the corresponding classical theorem in the case where the Kripke models force classical logic.

MSC:

03B20 Subsystems of classical logic (including intuitionistic logic)
03C40 Interpolation, preservation, definability
03C90 Nonclassical models (Boolean-valued, sheaf, etc.)
Full Text: DOI