[Proof Complexity] A Survey on Proof Complexity

[Amir Tabatabai]

Dear all,

I have recently written a chapter on proof complexity and its connection to
interpolation, available here:

https://arxiv.org/abs/2505.03002

This chapter will appear in the forthcoming book "Theory and Applications
of Craig Interpolation", edited by Balder ten Cate, Jean Christoph Jung,
Patrick Koopmann, Christoph Wernhard, and Frank Wolter.

The chapter serves as a survey of the basics of propositional proof
complexity, both classical and non-classical, with a particular emphasis on
the use of feasible interpolation to establish hardness results. It is
intended to be accessible to a broader audience familiar with proof theory,
though not necessarily with proof complexity. I assume only a basic
familiarity with propositional, modal, and first-order logic, as well as
foundational concepts from computational complexity, such as the complexity
classes NP and PSPACE. Any additional notions are introduced and explained
as needed.

I would greatly appreciate any comments, suggestions, corrections, or
general feedback you may have.

Best wishes,
Amir.