# Two-variable logic

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Two-variable_logic
> Markdown URL: https://mediated.wiki/source/Two-variable_logic.md
> Source: https://en.wikipedia.org/wiki/Two-variable_logic
> Source revision: 1110079464
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

In [mathematical logic](/source/Mathematical_logic) and [computer science](/source/Computer_science), **two-variable logic** is the [fragment](/source/Fragment_(logics)) of [first-order logic](/source/First-order_logic) where [formulae](/source/Formula_(logics)) can be written using only two different [variables](/source/Variable_(logics)).[1] This fragment is usually studied without [function symbols](/source/Function_symbol).

## Decidability

Some important problems about two-variable logic, such as [satisfiability](/source/Satisfiability_(logics)) and [finite satisfiability](/source/Finite_satisfiability_(logics)), are [decidable](/source/Decidability_(computer_science)).[2] This result generalizes results about the decidability of fragments of two-variable logic, such as certain [description logics](/source/Description_logic); however, some fragments of two-variable logic enjoy a much lower [computational complexity](/source/Computational_complexity_theory) for their satisfiability problems.

By contrast, for the three-variable fragment of first-order logic without function symbols, satisfiability is undecidable.[3]

## 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](/source/Counting_quantifiers),[4] and thus of [uniqueness quantification](/source/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 {\displaystyle n} neighbors, namely Φ = ∃ x ∃ ≥ n y E ( x , y ) {\displaystyle \Phi =\exists x\exists ^{\geq n}yE(x,y)} . Without counting quantifiers n + 1 {\displaystyle 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](/source/Colour_refinement_algorithm)) 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 {\displaystyle C^{2}} type, that is, they satisfy the same formulas in two-variable logic with counting.[5]

## References

1. **[^](#cite_ref-1)** L. Henkin. *Logical systems containing only a finite number of symbols*, Report, Department of Mathematics, University of Montreal, 1967

1. **[^](#cite_ref-2)** E. Grädel, P.G. Kolaitis and M. Vardi, *On the Decision Problem for Two-Variable First-Order Logic*, The Bulletin of Symbolic Logic, Vol. 3, No. 1 (Mar., 1997), pp. 53-69.

1. **[^](#cite_ref-3)** A. S. Kahr, Edward F. Moore and Hao Wang. *Entscheidungsproblem Reduced to the ∀ ∃ ∀ Case*, 1962, noting that their ∀ ∃ ∀ formulas use only three variables.

1. **[^](#cite_ref-4)** E. Grädel, M. Otto and E. Rosen. *Two-Variable Logic with Counting is Decidable.*, Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 1997.

1. **[^](#cite_ref-5)** Grohe, Martin. "Finite variable logics in descriptive complexity theory." Bulletin of Symbolic Logic 4.4 (1998): 345-398.

---
Adapted from the Wikipedia article [Two-variable logic](https://en.wikipedia.org/wiki/Two-variable_logic) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Two-variable_logic?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.