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. This fragment is usually studied without function symbols.

Decidability

Some important problems about two-variable logic, such as satisfiability and finite satisfiability, are decidable. 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.

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, 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 neighbors, namely. Without counting quantifiers 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 algorithm. Given two graphs, then any two nodes have the same stable color in color refinement if and only if they have the same type, that is, they satisfy the same formulas in two-variable logic with counting.