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 $n$ neighbors, namely $\Phi = \exists x \exists^{\geq n} y E(x,y)$. Without counting quantifiers $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 $C^2$ type, that is, they satisfy the same formulas in two-variable logic with counting.Grohe, Martin. "Finite variable logics in descriptive complexity theory." Bulletin of Symbolic Logic 4.4 (1998): 345-398.

References

Model theory
Systems of formal logic