Syntactic Preservation Theorems for Intuitionistic Predicate Logic
Fleischmann, Jonathan
Notre Dame J. Formal Logic, Tome 51 (2010) no. 1, p. 225-245 / Harvested from Project Euclid
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.
Publié le : 2010-04-15
Classification:  Kripke models,  intuitionistic predicate logic,  preservation theorems,  formula hierarchies,  Keisler Sandwich Theorem,  03B20,  03C40,  03C90,  03F55
@article{1276284784,
     author = {Fleischmann, Jonathan},
     title = {Syntactic Preservation Theorems for Intuitionistic Predicate Logic},
     journal = {Notre Dame J. Formal Logic},
     volume = {51},
     number = {1},
     year = {2010},
     pages = { 225-245},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1276284784}
}
Fleischmann, Jonathan. Syntactic Preservation Theorems for Intuitionistic Predicate Logic. Notre Dame J. Formal Logic, Tome 51 (2010) no. 1, pp.  225-245. http://gdmltest.u-ga.fr/item/1276284784/