Model-theoretic characterization of predicate intuitionistic formulas

TL;DR

This paper characterizes when first-order formulas correspond to intuitionistic predicate formulas using invariance under asimulations and k-asimulations, extending model-theoretic tools to predicate logic.

Contribution

It extends the notions of asimulation and k-asimulation to predicate logic and characterizes intuitionistic formulas via invariance under these relations.

Findings

First-order formulas equivalent to intuitionistic translations are invariant under k-asimulations.

Invariance under asimulations characterizes intuitionistic formulas.

Results hold over classes of intuitionistic models with constant domains.

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).