On the Decision Problem for Two-Variable First-Order Logic

Gradel, Kolaitis, Vardi

logic first order two-variable complexity decidability

@article{gradel:symbolic-1997,
  title={On the Decision Problem for Two-Variable First-Order Logic},
  author={Gr\"adel, E. and Kolaitis, P.G. and Vardi, M.Y.},
  journal={Bulletin of Symbolic Logic},
  pages={53--69},
  year={1997},
  publisher={Association for Symbolic Logic}
}

Fragment of first order logic consisting of all relational sentences with at most two distinct variables

• Decidability from Mortimer, 1975, via finite model property
  • Showed that model size is at most doubly exponential in the size of the sentence
• This paper shows that model's size is at most exponential in size of sentence
  • With or without equality
  • Making satisfiability here NEXPTIME-complete

Modal logic: Logic of "necessity" and "possibility" where the two can be interpreted in many ways

• Propositional model logic is a fragment of of FO^2 without equality

Presence or absence of equality may greatly affect decidability and complexity

• Example: G\"odel class
  • \exists * \forall\forall\exists * without equality is decidable
  • Even minimal fragment \forall\forall\exists is undecidable with equality
• Example: Ackermann class
  • \exists * \forall\exists * without equality is EXPTIME
  • With equality it is NEXPTIME