Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Proof Complexity and Feasible Interpolation

Amirhossein Akbar Tabatabai

TL;DR

The chapter surveys propositional proof complexity with a focus on feasible interpolation as a tool for transferring lower bounds from computational complexity to proof length. It develops the descriptive and computational power of propositional encodings of finite structures, then analyzes a spectrum of proof systems (LK, LJ, Resolution, CP, NS, Frege variants) through simulations and p-boundedness, linking these notions to NP/PSPACE assumptions. Central to the narrative is Craig interpolation and its non-classical generalizations (PDIP/MDIP), which, when hard, yield lower bounds on proof length under feasible interpolation, especially in the presence of hard disjoint NP pairs arising from cryptographic assumptions like RSA and Diffie–Hellman. The text culminates in classical FI results for LK^−, R, and CP, and non-classical FI results for IPC-like and modal logics (GL, S4), highlighting how feasibility of interpolants shapes automatisation and lower bounds across both classical and non-classical logics.

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.

Proof Complexity and Feasible Interpolation

TL;DR

The chapter surveys propositional proof complexity with a focus on feasible interpolation as a tool for transferring lower bounds from computational complexity to proof length. It develops the descriptive and computational power of propositional encodings of finite structures, then analyzes a spectrum of proof systems (LK, LJ, Resolution, CP, NS, Frege variants) through simulations and p-boundedness, linking these notions to NP/PSPACE assumptions. Central to the narrative is Craig interpolation and its non-classical generalizations (PDIP/MDIP), which, when hard, yield lower bounds on proof length under feasible interpolation, especially in the presence of hard disjoint NP pairs arising from cryptographic assumptions like RSA and Diffie–Hellman. The text culminates in classical FI results for LK^−, R, and CP, and non-classical FI results for IPC-like and modal logics (GL, S4), highlighting how feasibility of interpolants shapes automatisation and lower bounds across both classical and non-classical logics.

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 and . Any additional concepts will be introduced and explained as needed.
Paper Structure (21 sections, 47 theorems, 25 equations, 2 figures, 1 table)

This paper contains 21 sections, 47 theorems, 25 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Propositional Incompleteness
  3. Feasible Interpolation
  4. Outline of the Chapter
  5. Preliminaries
  6. The Propositional World
  7. Descriptive Power
  8. Computational Power
  9. A Bit of Cryptography
  10. Disjoint $\mathbf{NP}$ Pairs
  11. Proof Systems
  12. Simulations and Relative Efficiency
  13. Absolute Efficiency
  14. Interpolants and their Computation
  15. Computing Craig Interpolants in Classical Logic
  16. ...and 6 more sections

Key Result

Theorem 3.5

Let $L \in \mathbf{NP}$ be a language. Then, there exists a one-sorted first-order language $\mathcal{L}$ with no function symbols and a first-order formula $\phi(\bar{S}, R)$, where $R$ is a unary predicate such that $(\{1, \ldots, n\}, R_w) \vDash \exists \bar{S} \, \phi(\bar{S}, R)$ iff $w \in L$

Figures (2)

  • Figure 1: The sequent calculus $\mathbf{LK}$
  • Figure 2: Some proof systems for $\mathsf{CPC}$krajivcek2019proof. If there is a line between two proof systems, the higher one simulates the lower. For the proof systems in the blue region, an exponential lower bound is known. For those in the red region, it is not even known whether they are not p-bounded.

Theorems & Definitions (131)

  • Example 3.1
  • Example 3.2
  • Example 3.3
  • Example 3.4: Propositional Pigeonhole Principle
  • Theorem 3.5: Fagin immerman1998descriptive
  • Theorem 3.6
  • proof
  • Definition 3.7: $\mathfrak{L}$-Circuit
  • Definition 3.8
  • Remark 3.9
  • ...and 121 more