Model-theoretic characterization of predicate intuitionistic formulas
arXiv:1202.1195 · doi:10.1093/logcom/ext014
Abstract
Notions of asimulation and k-asimulation introduced in [Olkhovikov, 2011] are extended onto the level of predicate logic. We then prove that a first-order formula is equivalent to a standard translation of an intuitionistic predicate 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 predicate 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 predicate formula over a class of intuitionistic models (intuitionistic models with constant domain) iff it is invariant with respect to asimulations between intuitionistic models (intuitionistic models with constant domain).
Cited by in corpus (5)
- On generalized Van-Benthem-type characterizations
- Expressive power of basic modal intuitionistic logic as a fragment of classical FOL
- A van Benthem Theorem for Atomic and Molecular Logics
- A Lindström theorem for intuitionistic propositional logic
- Craig interpolation theorem fails in bi-intuitionistic predicate logic