# 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