On Logics with Two Variables

Gradel and Otto

modal logic first order description complexity expressiveness decidability

@article{gradel:tcs-1999,
  author={Erich Gr\"adel and Martin Otto},
  title={On Logics with Two Variables},
  journal={Theoretical Computer Science},
  year={1999},
  volume={224},
  pages={73--113}
}

Result from Mortimer: Two-variable fragment of first order logic (FO^2) is decidable for satisfiability, via finite model property

Many propositional model logics can be embedded into this fragment

• Description logics, computation tree logic (CTL), etc

Extending modal logic is more robust in respect to decidability than FO^2

Being two-variable requires being verifiable by successively examining pairs of objects; it does not require a larger view of the structure

Fo^2 with counting is decidable

Most interesting extensions of FO^2 are not decidable

• Do not have finite model property, though that is not necessary
• It is probably because they fail the tree-model property

Addition of transitive closure renders FO^2 undecidable