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.
Decidability
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]
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,[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 [math]\displaystyle{ n }[/math] neighbors, namely [math]\displaystyle{ \Phi = \exists x \exists^{\geq n} y E(x,y) }[/math]. Without counting quantifiers [math]\displaystyle{ n+1 }[/math] 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) algorithm. Given two graphs, then any two nodes have the same stable color in color refinement if and only if they have the same [math]\displaystyle{ C^2 }[/math] type, that is, they satisfy the same formulas in two-variable logic with counting.[5]
References
- ↑ L. Henkin. Logical systems containing only a finite number of symbols, Report, Department of Mathematics, University of Montreal, 1967
- ↑ 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.
- ↑ A. S. Kahr, Edward F. Moore and Hao Wang. Entscheidungsproblem Reduced to the ∀ ∃ ∀ Case, 1962, noting that their ∀ ∃ ∀ formulas use only three variables.
- ↑ 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.
- ↑ Grohe, Martin. "Finite variable logics in descriptive complexity theory." Bulletin of Symbolic Logic 4.4 (1998): 345-398.
 |  |
