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.