arXiv · 1207.4414
Model-theoretic characterization of intuitionistic propositional formulas
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 intuitionistically equivalent to a standard translation of an intuitionistic propositional formula iff it is invariant with respect to asimulations between intuitionistic models.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Grigory K. Olkhovikov. 2012-07-18. Model-theoretic characterization of intuitionistic propositional formulas. https://doi.org/10.1017/s1755020312000342
Cite the original work for its findings. Save a collection to share your selection of sources.