By contrast, for the three-variable fragment of first-order logic without function symbols, satisfiability is undecidable.
[3] 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
There is a strong connection between two-variable logic and the Weisfeiler-Leman (or color refinement) algorithm.