The Boundedness Problem for Monadic Universal First-Order Logic
The Boundedness Problem for Monadic Universal First-Order Logic
复制标题
一元通用一阶逻辑的有界性问题
DOI：
10.1109/lics.2006.50
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
M. Otto
中科院分区：
文献类型：
--
作者：
M. Otto
将FO公式上最小不动点的一元有界性问题视为一个判定问题：给定一个公式phi（X，x），在X中为正，判定基于phi的最小不动点递归是否存在一致有限界.已知FO的一些片段具有可判定的有界性问题;已知许多片段的有界性是不可判定的。我们在这里表明，一元有界性是可判定的纯泛FO公式没有平等，其中每个非递归谓词发生在只有一个极性（例如，消极的）。的限制被证明是必不可少的：挥舞的极性约束或允许积极出现的平等，一元有界性问题的普遍公式变得不可判定。主要结果是基于一个模型理论分析涉及的想法，从模态和保护逻辑和减少一元二阶理论的树木
We consider the monadic boundedness problem for least fixed points over FO formulae as a decision problem: Given a formula phi(X, x), positive in X, decide whether there is a uniform finite bound on the least fixed point recursion based on phi. 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 a reduction to the monadic second-order theory of trees