Definition and Syntax
FO² is the fragment of first-order logic that uses at most two distinct individual-variable symbols, conventionally x and y. Variables may be bound repeatedly. Here we consider relational signatures with equality, but without constant or function symbols.
Semantics and Example
FO² has ordinary first-order semantics; only its syntax is restricted.
\forall x\,\exists y\,(R(x,y)\land x\ne y)
Every element has an R-successor distinct from itself. Restricting the language to two variable symbols does not restrict quantifier depth or model size to two.
Properties and Complexity
FO² has the finite model property: every satisfiable sentence has a finite model of at most singly exponential size in the length of the sentence. Satisfiability and finite satisfiability are NEXPTIME-complete [1], with the relational signature considered part of the input.
The standard translation of basic modal logic K can be expressed using two reusable variable symbols. In contrast, the guarded fragment restricts the form of quantification.
References
- Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi (1997). On the Decision Problem for Two-Variable First-Order Logic. Bulletin of Symbolic Logic 3(1), 53–69. DOI.