## Paper: Two-variable logic with counting is decidable (at LICS 1997)

**Erich Grädel Martin Otto Eric Rosen**

### Abstract

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{GrdelOttoRosen-Twovariablelogicwit, author = {Erich Grädel and Martin Otto and Eric Rosen}, title = {Two-variable logic with counting is decidable}, booktitle = {Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS 1997)}, year = {1997}, month = {June}, pages = {306--317}, location = {Warsaw, Poland}, publisher = {IEEE Computer Society Press} }