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

Authors: 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}
  }