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.
