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.
Keywords
Cite
@article{arxiv.1207.4414,
title = {Model-theoretic characterization of intuitionistic propositional formulas},
author = {Grigory K. Olkhovikov},
journal= {arXiv preprint arXiv:1207.4414},
year = {2015}
}
Comments
16 pages, 0 figures. arXiv admin note: substantial text overlap with arXiv:1202.1195