Model-theoretic characterization of intuitionistic propositional formulas

TL;DR

This paper characterizes intuitionistic propositional formulas using model-theoretic notions like k-asimulation and asimulation, establishing invariance conditions that correspond to intuitionistic equivalence in first-order logic.

Contribution

It introduces notions of k-asimulation and asimulation and proves their role in characterizing intuitionistic propositional formulas via invariance in first-order logic.

Findings

A first-order formula is equivalent to an intuitionistic translation iff invariant under k-asimulations.

A first-order formula is equivalent to an intuitionistic translation iff invariant under asimulations.

Intuitionistic equivalence corresponds to invariance under asimulations between models.

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.