Paper: Two-variable logic with counting is decidable (at LICS 1997)
Authors: Erich Graedel Martin Otto Eric RosenAbstract
We prove that the satisfiability and the finite satisfiability problems for C^2 are decidable. C^2 is first-order logic with only two variables in the presence of arbitrary counting quantifiers, "there exist at least m elements x", for m a natural number. It considerably extends L^2, plain first-order with only two variables, which is known to be decidable by a result of Mortimer's. Unlike L^2, C^2 does not have the finite model property.
BibTeX
@InProceedings{GraedelOttoRosen-Twovariablelogicwit, author = {Erich Graedel and Martin Otto and Eric Rosen}, title = {Two-variable logic with counting is decidable}, booktitle = {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997}, year = 1997, editor = {Glynn Winskel}, month = {June}, pages = {306--317}, location = {Warsaw, Poland}, publisher = {IEEE Computer Society Press} }