Proof Complexity and Feasible Interpolation

TL;DR

This survey introduces propositional proof complexity with a focus on feasible interpolation, a method for constructing hard theorems that demonstrate super-polynomial proof lengths in various proof systems.

Contribution

It provides an accessible overview of proof complexity and the feasible interpolation method, highlighting its role in establishing lower bounds for proof systems across different logics.

Findings

Feasible interpolation helps construct hard theorems with super-polynomial proof lengths.

The survey clarifies key proof complexity concepts for a broad audience.

It connects proof complexity with computational complexity classes like NP and PSPACE.

Abstract

This is a survey on propositional proof complexity aimed at introducing the basics of the field with a particular focus on a method known as feasible interpolation. This method is used to construct "hard theorems" for several proof systems for both classical and non-classical logics. Here, a "hard theorem" refers to a theorem in the logic whose shortest proofs are super-polynomially long in the length of the theorem itself. To make this survey more accessible, we only assume a basic familiarity with propositional, modal, and first-order logic, as well as a basic understanding of the key concepts in computational complexity, such as the definitions of the classes $\mathbf{NP}$ and $\mathbf{PSPACE}$. Any additional concepts will be introduced and explained as needed.