Submodels of Kripke models |
| |
Authors: | Albert Visser |
| |
Institution: | (1) Department of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS Utrecht, The Netherlands. e-mail: albert.visser@phil.uu.nl, NL |
| |
Abstract: | A Kripke model ? is a submodel of another Kripke model ℳ if ? is obtained by restricting the set of nodes of ℳ. In this paper we show that the class of
formulas of Intuitionistic Predicate Logic that is preserved under taking submodels of Kripke models is precisely the class
of semipositive formulas. This result is an analogue of the Łoś-Tarski theorem for the Classical Predicate Calculus.
In Appendix A we prove that for theories with decidable identity we can take as the embeddings between domains in Kripke models
of the theory, the identical embeddings. This is a well known fact, but we know of no correct proof in the literature. In
Appendix B we answer, negatively, a question posed by Sam Buss: whether there is a classical theory T, such that ℋT is HA. Here ℋT is the theory of all Kripke models ℳ such that the structures assigned to the nodes of ℳ all satisfy T in the sense of classical model theory.
Received: 4 February 1999 / Published online: 25 January 2001 |
| |
Keywords: | or phrases: Kripke models – Intuitionistic logic – Heyting arithmetic |
本文献已被 SpringerLink 等数据库收录! |
|