## Paper: On the Boundedness Problem for Two-Variable First-Order Logic (at LICS 1998)

**Phokion G. Kolaitis Martin Otto**

### Abstract

A positive first-order formula is bounded if the sequence of its
stages converges to the least fixed point of the formula within a fixed
finite number of steps independent of the input structure. The
boundedness problem for a fragment C of first-order logic is the
following decision problem: given a positive formula in L, is it
bounded? In this paper, we investigate the boundedness problem for
two-variable first-order logic FO^{2}. As a general rule,
FO^{2} is a well-behaved fragment of first-order logic, since it
possesses the finite-model property and has a decidable satisfiability
problem. Nonetheless, our main result asserts that the boundedness
problem for FO^{2} is undecidable, even when restricted to
negation-free and equality-free formulas φ(X, x) in which x is the
only free variable and X is a monadic relation symbol that occurs within
the scopes of universal quantifiers only. This undecidability result
contrasts sharply with earlier results asserting the decidability of
boundedness for monadic Datalog programs, which amounts to the
decidability of boundedness for negation-free and equality-free
existential first-order formulas ψ(X, x) in which x is the only free
variable and X is a monadic relation symbol. We demonstrate that our
main result has certain applications to circumscription, the most
well-developed formalism of nonmonotonic reasoning. Specifically, using
the undecidability of boundedness for FO^{2}, we show that it is
an undecidable problem to tell whether the circumscription of a given FO
^{2}-formula is equivalent to a first-order formula. In
contrast, the circumscription of every FO^{1}-formula is
equivalent to a first-order formula

### BibTeX

@InProceedings{KolaitisOtto-OntheBoundednessPro, author = {Phokion G. Kolaitis and Martin Otto}, title = {On the Boundedness Problem for Two-Variable First-Order Logic}, booktitle = {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)}, year = {1998}, month = {June}, pages = {513--524}, location = {Indianapolis, IN, USA}, publisher = {IEEE Computer Society Press} }