On the boundedness problem for two-variable first-order logic
On the boundedness problem for two-variable first-order logic
复制标题
关于二变量一阶逻辑的有界问题
DOI：
--
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
M. Otto
中科院分区：
文献类型：
--
作者：
Phokion G. Kolaitis;M. Otto
如果其阶段的序列在固定有限数量的步骤中收敛到公式的最小固定点，则构成正式公式。一阶逻辑的片段C的界限问题是以下决策问题：鉴于L中的正公式，它是否有限？在本文中，我们研究了两种一阶逻辑fo/sup 2/的界限问题。一般而言，FO/ SUP 2/是一阶逻辑的行为良好的片段，因为它具有有限模型属性，并且具有可决定性的满足性问题。但是，我们的主要结果断言，即使仅限于无否定和无均等的公式/spl phi/（x，x），x，x，x，x是x是唯一的自由变量和x是仅在通用量词的范围内发生的单一关系符号。这种不可证明的结果与早期结果截然形成鲜明对比。是唯一的自由变量，x是一个单一的关系符号。我们证明，我们的主要结果具有某些应用于限制的应用，这是非单调推理的最发达的形式主义。具体而言，使用fo/sup 2/的界限不确定性，我们表明，要确定给定的FO/SUP 2/-formula的外观是否等于一阶公式是一个不可避免的问题。相反，每个FO/SUP 1/-Formula的限制都等于一阶公式。
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/sup 2/. As a general rule, FO/sup 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/sup 2/ is undecidable, even when restricted to negation-free and equality-free formulas /spl phi/(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 /spl psi/(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/sup 2/, we show that it is an undecidable problem to tell whether the circumscription of a given FO/sup 2/-formula is equivalent to a first-order formula. In contrast, the circumscription of every FO/sup 1/-formula is equivalent to a first-order formula.