Paper: The boundedness problem for monadic universal first-order logic (at LICS 2006)

Authors: Martin Otto

Abstract

We consider the monadic boundedness problem for least fixed points over FO formulae as a decision problem: Given a formula (X, x), positive in X, decide whether there is a uniform finite bound on the least fixed point recursion based on . Few fragments of FO are known to have a decidable boundedness problem; boundedness is known to be undecidable for many fragments. We here show that monadic boundedness is decidable for purely universal FO formulae without equality in which each non-recursive predicate occurs in just one polarity (e.g., only negatively). The restrictions are shown to be essential: waving either the polarity constraint or allowing positive occurrences of equality, the monadic boundedness problem for universal formulae becomes undecidable. The main result is based on a model theoretic analysis involving ideas from modal and guarded logics and

BibTeX

  @InProceedings{Otto-Theboundednessprobl,
    author = 	 {Martin Otto},
    title = 	 {The boundedness problem for monadic universal first-order logic},
    booktitle =  {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)},
    year =	 {2006},
    month =	 {August}, 
    pages =      {37--46},
    location =   {Seattle, Washington, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }