__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.