Two-variable logic: Difference between revisions

Revision as of 21:09, 24 August 2017

Revision as of 09:17, 14 June 2019

Line 1:

{{ref improve|date=August 2014}}

In [[mathematical logic]] and [[computer science]], '''two-variable logic''' is the [[fragment (logics)|fragment]] of [[first-order logic]] where [[formula (logics)|formulae]] can be written using only two different [[variable (logics)|variable]]s <ref> L. Henkin. ''Logical systems containing only a finite number of symbols'', Report, Department of Mathematics, University of Montreal, 1967</ref>. This fragment is usually studied without [[function symbol]]s.

== Decidability ==

Some important problems about two-variable logic, such as [[satisfiability (logics)|satisfiability]] and [[finite satisfiability (logics)|finite satisfiability]], are [[decidability (computer science)|decidable]].<ref>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.</ref> This result generalizes results about the decidability of fragments of two-variable logic, such as certain [[description logic]]s; however, some fragments of two-variable logic enjoy a much lower [[Computational complexity theory|computational complexity]] for their satisfiability problems.

Line 11:

== 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]]<ref>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.</ref>, 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 ==