We consider the abstract notion of a propositional proof system and present Cook's theorem, relating the complexity of propositional proofs to fundamental questions in complexity theory, P vs NP and coNP vs NP. Typical systems from undergraduate courses are considered and some basic complexity properties are presented; in particular we expose the complexity gap between systems with cut and cut-free systems.

In order to better understand the complexity of systems with cut, various restrictions on proofs have been proposed. The most well-studied approach is the bounding of depth of formulae occurring in a proof, motivated by circuit complexity theory. We outline textbook results on the complexity of such systems and briefly discuss connections with bounded arithmetic.

Finally we consider a modern approach motivated by the deep inference methodology. We prove the equivalence of these systems to sequent proofs with various restrictions on cut-formulae, and present recent complexity results.

A running example throughout these talks will be propositional encodings of the pigeonhole principle, and how the size of proofs of this encoding varies amongst propositional proof systems.

**Frege and Gentzen systems.**
Robustness of Frege, Dag-like proofs and tree-like proofs, Equivalence of Frege and Gentzen systems, Cost of cut-elimination, Cost of dag-elimination, Polynomial-size proofs of the pigeonhole principle.

**Bridging the gap: bounded-depth approach.**
Bounded-depth Frege systems, Relationship to logic and complexity theory, Special case of resolution, Exponential lower bound on proofs of the pigeonhole principle.

**Bridging the gap: analytic deep inference.**
Analytic deep inference systems, Formulation as restrictions on cut-formulae, Relative complexity results, Quasipolynomial-size proofs of the pigeonhole principle.

Cook, Stephen A. "The complexity of theorem-proving procedures." In *Proceedings of the third annual ACM symposium on Theory of computing*, pp. 151-158. ACM, 1971.

Buss, Samuel R. "Polynomial size proofs of the propositional pigeonhole principle." *Journal of Symbolic Logic* (1987): 916-927.

Paris, Jeff, and A.J. Wilkie, "Delta-0 sets and induction." *Proceedings of the Jadwisin Logic Conference*, pp.237-248. Leeds University Press, 1981.

Pitassi, Toniann, Paul Beame, and Russell Impagliazzo. "Exponential lower bounds for the pigeonhole principle." *Computational complexity* 3, no. 2 (1993): 97-140.

Krajicek, Jan. *Bounded arithmetic, propositional logic and complexity theory*. Cambridge University Press, 1995.

Atserias, Albert, Nicola Galesi, and Ricard Gavalda. "Monotone proofs of the pigeon hole principle." *Mathematical Logic Quarterly* 47, no. 4 (2001): 461-474.

Bruscoli, Paola, and Alessio Guglielmi. "On the proof complexity of deep inference." *ACM Transactions on Computational Logic (TOCL)* 10, no. 2 (2009): 14.

Das, Anupam. "Complexity of deep inference via atomic flows." In *How the World Computes*, pp. 139-150. Springer Berlin Heidelberg, 2012.