Model-theoretic characterization of predicate intuitionistic formulas
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).
Keywords
Cite
@article{arxiv.1202.1195,
title = {Model-theoretic characterization of predicate intuitionistic formulas},
author = {Grigory K. Olkhovikov},
journal= {arXiv preprint arXiv:1202.1195},
year = {2015}
}