Content deleted Content added
m →Counting quantifiers: typo in formula |
|||
Line 13:
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.
Counting quantifiers actually improve the expressiveness of finite-variable logics as they allow to say that there is a node with <math>n</math> neighbors, namely <math>\Phi = \exists x \exists^{\geq n} y E(x,y)</math>. Without counting quantifiers <math>n+1</math> variables are needed for the same formula.
== Connection to the Weisfeiler-Leman algorithm ==
| |||