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, and one of its main points is that some important problems about it, such as satisfiability and finite satisfiability, are decidable.

What is more, the two-variable fragment of first-order logic with no function symbols is known to be decidable even with the addition of counting quantifiers. This is a more powerful result, as counting quantifiers for high numerical values are not expressible in that logic.