# 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.

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]}

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.