On the boundedness problem for two-variable first-order logic

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². As a general rule, FO² 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² 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², we show that it is an undecidable problem to tell whether the circumscription of a given FO ²-formula is equivalent to a first-order formula. In contrast, the circumscription of every FO¹-formula is equivalent to a first-order formula