arXiv · 1202.1195
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).
Explore related subjects
Keep this discovery
Grigory K. Olkhovikov. 2012-02-02. Model-theoretic characterization of predicate intuitionistic formulas. https://doi.org/10.1093/logcom/ext014
Cite the original work for its findings. Save a collection to share your selection of sources.