Two-variable logic
 | This article needs additional citations for verification. (August 2014) |
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.
Decidability
Some important problems about two-variable logic, such as satisfiability and finite satisfiability, are decidable.[1] 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.[2]
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, and thus of uniqueness quantification. This is a more powerful result, as counting quantifiers for high numerical values are not expressible in that logic.
References
- ^ 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.
 | This logic-related article is a stub. You can help Wikipedia by expanding it. |
 | This computer science article is a stub. You can help Wikipedia by expanding it. |