Two-variable logic with counting

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.

One of the main points is that 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.

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.

...
Wikipedia