Mathematical Sciences: Proof Theory and Computational Complexity

塞缪尔·巴斯的研究涉及数学逻辑的形式系统和低级复杂性以及这些学科之间的相互关系。要研究的逻辑系统包括算术片段，特别是有界算术，纯一阶逻辑和命题逻辑。要研究的低复杂度类包括交替对数时间和多项式时间层次。他特别关注在计算复杂性和形式系统的证明理论之间发展新的和富有成效的联系。过去的研究已经在这些领域之间建立了密切的联系。该项目主要关注(1)与各种计算复杂性类密切相关的证明理论强度的形式理论；(2)一阶和命题证明的结构，特别是证明的长度。证明论关注的是证明的一些性质，如它们的长度、正确性被理解和被认为是理所当然的。因此，一个典型的结果可能断言命题P是一个比命题Q更深的结果，因为P的任何证明（在一个特定的形式系统中）都比Q的某些已知证明（在同一系统中）长。一个稍微复杂的结果类型考虑命题序列P1， P2, P3，…， Pn，…，所有在形式系统F和形式系统G中均可证明的命题，例如，如果这些命题在F中的最佳证明的长度以n的平方增长，而它们在G中的最佳证明的长度以n的指数增长，那么F似乎是一个比g更强大的系统。巴斯已经找到了将这种性质的问题与计算机科学家已经研究过的算术函数的复杂性类联系起来的方法。

The research of Samuel Buss deals with formal systems of mathematical logic and with low-level complexity and the interrelationships between these subjects. The logical systems to be studied include fragments of arithmetic, especially bounded arithmetic, and pure first-order logic and propositional logic. The low-level complexity classes to be studied include alternating log time and the polynomial time hierarchy. He is particularly concerned with developing new and fruitful connections between computational complexity and the proof theory of formal systems. Past research has already established intimate connections between these areas. This project concerns primarily (1) formal theories with proof-theoretic strength closely related to various computational complexity classes and (2) the structure of first- order and propositional proofs, especially, the lengths of proofs. Proof theory is concerned with such properties of proofs as their length, correctness being understood and taken for granted. Thus a typical result might assert that the proposition P is a deeper result than the proposition Q in the sense that any proof of P (in a specific formal system) is longer than some known proof of Q (in the same system). A slightly more complicated type of result considers a sequence of propositions P1, P2, P3, ..., Pn, ..., all provable both in the formal system F and in the formal system G. If, for example, the lengths of the best proofs of these propositions in F grow in length as the square of n, while their best proofs in G grow exponentially in n, then it would seem that F is a more powerful system than G. Buss has found ways to relate questions of this nature to complexity classes of arithmetic functions that have already been studied by computer scientists.