Talk slides.
Samuel R. Buss.
"Expressibility and Derivability, and the Complexity of Proofs"
PhilMath Intersem 2011.
June 27, 2011
Download talk slides: PDF.
Abstract: It is a general principle that the power of a formal proof system can be directly tied to the expressive power of its formulas. However, there are notable exceptions, and a number of important related open questions. Indeed, there are proof systems that can express the concepts needed for the proof of a theorem, but still cannot prove, or are not known to prove, the theorem efficiently. Conversely, it can happen that a proof system is unable to express the concepts that are seemingly needed for a theorem, but is still able to state and efficiently prove the theorem. We discuss examples of these, along with related questions about the complexity of proofs. We discuss mostly weak proof systems, including propositional logic, but also examples in first order logic. Particular attention will be paid to open problems.