Two-variable logic

In mathematical logic and computer science, two-variable logic is the fragment of first-order logic where formulae can be written using only two different variables.^[1] This fragment is usually studied without function symbols.

Decidability

Some important problems about two-variable logic, such as satisfiability and finite satisfiability, are decidable.^[2] This result generalizes results about the decidability of fragments of two-variable logic, such as certain description logics; however, some fragments of two-variable logic enjoy a much lower computational complexity for their satisfiability problems.

By contrast, for the three-variable fragment of first-order logic without function symbols, satisfiability is undecidable.^[3]

Counting quantifiers

The two-variable fragment of first-order logic with no function symbols is known to be decidable even with the addition of counting quantifiers,^[4] and thus of uniqueness quantification. This is a more powerful result, as counting quantifiers for high numerical values are not expressible in that logic.

Counting quantifiers actually improve the expressiveness of finite-variable logics as they allow to say that there is a node with ${\displaystyle n}$ neighbors, namely ${\displaystyle \Phi =\exists x\exists ^{\geq n}yE(x,y)}$. Without counting quantifiers ${\displaystyle n+1}$ variables are needed for the same formula.

Connection to the Weisfeiler-Leman algorithm

There is a strong connection between two-variable logic and the Weisfeiler-Leman (or color refinement) algorithm. Given two graphs, then any two nodes have the same stable color in color refinement if and only if they have the same ${\displaystyle C^{2}}$ type, that is, they satisfy the same formulas in two-variable logic with counting.^[5]

References

1. L. Henkin. Logical systems containing only a finite number of symbols, Report, Department of Mathematics, University of Montreal, 1967
2. E. Grädel, P.G. Kolaitis and M. Vardi, On the Decision Problem for Two-Variable First-Order Logic, The Bulletin of Symbolic Logic, Vol. 3, No. 1 (Mar., 1997), pp. 53-69.
3. A. S. Kahr, Edward F. Moore and Hao Wang. Entscheidungsproblem Reduced to the ∀ ∃ ∀ Case, 1962, noting that their ∀ ∃ ∀ formulas use only three variables.
4. E. Grädel, M. Otto and E. Rosen. Two-Variable Logic with Counting is Decidable., Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 1997.
5. Grohe, Martin. "Finite variable logics in descriptive complexity theory." Bulletin of Symbolic Logic 4.4 (1998): 345-398.