Model-theoretic characterization of intuitionistic predicate formulas
Grigory K. Olkhovikov · Journal of Logic and Computation · 2013
The article introduces notions of first-order asimulation and first-order k-asimulation, which extend notions of asimulation and k-asimulation introduced in Olkhovikov (2012, Review of Symbolic Logic, 6, 348–365) onto the level of intuitionistic 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 first-order 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 first-order 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 first-order asimulations between intuitionistic models (intuitionistic models with constant domain).