The Limits of Decidability: Counting, Transitivity, Equivalence

一阶逻辑是一种形式化语言，用于描述对象和数据的结构化集成。使用一阶逻辑来指定、查询和操作这种结构化数据现在牢牢地植根于广泛的学术学科的理论和实践中。因此，自动化一阶逻辑中的演绎推理过程是计算机科学中的一个核心挑战。然而，使用一阶逻辑进行推理是众所周知的不可判定的：原则上不可能编写一个计算机程序来可靠地确定使用这种形式主义可以表达的所有逻辑结果。另一方面，长期以来，人们一直认为，通过以各种方式限制一阶逻辑的语言，我们获得了恢复可判断性的逻辑的“片段”。此外，我们观察到了表达能力和计算可管理性之间的权衡：片段越小-即表达能力越弱-就越容易推理。这里提出的研究将调查一阶逻辑的几个非常有表现力的片段-那些接近可判断性上限的片段-并确定它们的可判断性/计算复杂性。我们以三个已知可判定的一阶逻辑片段为出发点：‘双变量片段’、‘守卫片段’和‘凹槽片段’。我们通过三种方式(分别或组合)考察了扩展这些逻辑的表达能力的效果。我们考虑的第一个扩展涉及数字量词，它允许我们对满足某些给定属性的对象的数量设置(上或下)界。我们考虑的第二个扩展涉及到及物关系的使用，如‘高于’或‘赚更多的钱’。(这种关系具有特殊的逻辑属性，在推理问题中需要考虑这些属性。)我们考虑的第三个扩展涉及使用等价关系，例如‘高度相同于’或‘具有相同的税号’。通过这种方式，我们获得了一阶逻辑的片段的集合，对于该一阶逻辑，目前对其推理是否可判定是开放的。对于那些我们证明是可判定的片段，我们将获得(作为证明的副产品)在所述片段内进行推理的算法；对于那些被证明为不可判定的片段，我们知道不存在这样的算法。此外，对于可判定的片段，我们可以量化它们内部推理的难度，甚至可以确定导致疑难案件的特定类型的公式。因此，我们的研究对使用一阶逻辑来描述、查询或操作结构化数据的企业做出了贡献。

First-order logic is a formal language for describing structured ensembles of objects and data. The use of first-order logic to specify, query and manipulate such structured data is now firmly embedded in the theory and practice of a wide range of academic disciplines. Automating the process of deductive reasoning in first-order logic is therefore a central challenge in Computer Science.However, reasoning with first-order logic is known to be undecidable: it is in principle impossible to write a computer program that can reliably determine all logical consequences expressible using this formalism. On the other hand, it has long been understood that, by restricting the language of first-order logic in various ways, we obtain 'fragments' of logic in which decidability is restored. Furthermore, we observe a trade-off between expressive power and computational manageability: the smaller a fragment is---i.e. the less expressive it is---the easier it is to reason in. The research proposed here will investigate several very expressive fragments of first-order logic---those near the upper limit of decidability---and determine their decidability/computational complexity.We take as our point of departure three fragments of first-order logic which are known to be decidable: the 'two-variable fragment', the 'guarded fragment' and the 'fluted fragment'. We investigate the effect of extending the expressive power of these logics in three ways (severally, or in combination). The first extension we consider involves numerical quantifiers, which allow us to place (upper or lower) bounds on how many objects satisfy some given property. The second extension we consider involves the use of transitive relations such as 'is taller than' or `earns more money then'. (Such relations have special logical properties that need to be taken into account in reasoning problems.) The third extension we consider involves the use of equivalence relations such as 'is the same height as' or 'has the same tax code as'. In this way, we obtain a collection of fragments of first-order logic for which it is currently open whether reasoning is decidable. We propose to resolve these open problems.For those fragments which we show to be decidable, we shall obtain (as a by-product of our proof) an algorithm for reasoning within the fragments in question; for those shown to be undecidable, we know that no such algorithm exists. Moreover, for the decidable fragments, we can quantify the difficulty of reasoning within them, and even identify the specific kinds of formulas that are responsible for the difficult cases. Thus, our research represents a contribution to the enterprise of using first-order logic to describe, query or manipulate structured data.