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 neighbors, namely . Without counting quantifiers 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 type, that is, they satisfy the same formulas in two-variable logic with counting[5].

gollark: You know, sometimes I'd actually want viewbombing. Zyus are evil.
gollark: Are you suggesting that viewbombers also AR or something?
gollark: I generally miss eggs by just clicking past to the next biome then suddenly noticing then going back.
gollark: I generally try to fully read descriptions before clicking them, which may be why I usually can't get anything.
gollark: They see "gold" and forget "wait, golds aren't actually described as gold".

References
  1. L. Henkin. Logical systems containing only a finite number of symbols, Report, Department of Mathematics, University of Montreal, 1967
  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.
  3. A. S. Kahr, Edward F. Moore and Hao Wang. Entscheidungsproblem Reduced to the ∀ ∃ ∀ Case, 1962, noting that their ∀ ∃ ∀ formulas use only three variables.
  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.
  5. Grohe, Martin. "Finite variable logics in descriptive complexity theory." Bulletin of Symbolic Logic 4.4 (1998): 345-398.


This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.