Article contents
MODEL-THEORETIC CHARACTERIZATION OF INTUITIONISTIC PROPOSITIONAL FORMULAS
Published online by Cambridge University Press: 19 March 2013
Abstract
Notions of k-asimulation and asimulation are introduced as asymmetric counterparts to k-bisimulation and bisimulation, respectively. It is proved that a first-order formula is equivalent to a standard translation of an intuitionistic propositional formula iff it is invariant with respect to k-asimulations for some k, and then that a first-order formula is equivalent to a standard translation of an intuitionistic propositional formula iff it is invariant with respect to asimulations. Finally, it is proved that a first-order formula is equivalent to a standard translation of an intuitionistic propositional formula over the class of intuitionistic Kripke models iff it is invariant with respect to asimulations between intuitionistic models.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 2013
References
BIBLIOGRAPHY
- 11
- Cited by