AF: Small: Logic and Computational Complexity

逻辑试图描述以某种受限格式描述的句子的性质。计算复杂性研究在计算机上解决给定数学问题所需的步骤数。尽管这两个主题看起来互不相关，但逻辑和计算复杂性在过去有着丰富的互动历史。费金的经典定理给出了NP的逻辑定义，这可能是该领域最早的联系之一。在有限逻辑和计算复杂性的结合点上的其他著名结果包括Immerman-Szelepsenyi定理，它表明非确定的对数空间在互补下是封闭的；以及Ajtai关于有限结构的某些公式的工作，该公式表明奇偶校验不是一阶可定义的(这被证明等同于Furst、Saxe和Sipser的结果，即奇偶校验没有恒定的深度、多项式大小的电路)。这些结果既有超前的逻辑，也有计算的复杂性。这个研究项目的灵感来自于该项目的学生调查人员Swastik Kopparty和Ben Rossman最近的工作，他们发现了这些领域之间的新联系，导致了几个新的结果。这个项目概述了逻辑和计算复杂性的交集中的新的进一步问题，并概述了在这些问题上取得进展的方法。一些具体问题包括：-一致对数深度电路的大小下界。-用任意模计数量词(特别是模组合)扩充的一阶逻辑难以实现的显式函数。-解线性系统的不可选算法。-多集语义下合取查询的包容问题的可判性。

Logic attempts to describe the nature of sentences that have descriptions in some restricted format. Computational complexity investigates the number of steps needed on a computer to solve a given mathematical problem. Despite the seemingly disjoint nature of the topics, Logic and Computational Complexity have had a rich history of interactions in the past. Fagin's classical theorem giving a logical definition of NP is probably one of the first connections in the area. Other celebrated results in the nexus of finite logic and computational complexity include the Immerman-Szelepsenyi theorem showing non-deterministic logspace is closed under complementation; and Ajtai's work on certain formulae on finite structures, which shows that parity is not first-order definable (which turns out to be equivalent to Furst, Saxe, and Sipser's result that parity does not have constant depth, polynomial size circuits). These results have advanced logic as well as computational complexity.This research project is inspired by recent work by the student investigators on this project, Swastik Kopparty and Ben Rossman who have unearthed new connections between these areas leading to several new results. This project outlines novel further questions in the intersection of logic and computational complexity and outlines methods that may be employed to make progress on these questions. Some specific questions include:- Size lower bounds for uniform logarithmic depth circuits.- Explicit functions that are hard for first-order logic augmented with arbitrary modular counting quantifiers (modulo composites in particular).- Choiceless algorithms for solving linear systems.- Decidability of the containment problem for conjunctive queries under multiset semantics.