The Cook-Reckhow definition

TL;DR

This paper revisits the foundational 1979 definition of proof complexity by Cook and Reckhow, highlighting key concepts like proof systems and p-simulations, and discusses their significance and open problems in the field.

Contribution

It clarifies the original definitions from Cook-Reckhow and discusses their impact on the development of proof complexity theory.

Findings

Identifies three key definitions: proof systems, p-simulations, and pigeonhole principle formulas.

Highlights the role of these definitions in establishing proof complexity as a research area.

Mentions open problems and related developments in proof complexity.

Abstract

The Cook-Reckhow 1979 paper defined the area of research we now call Proof Complexity. There were earlier papers which contributed to the subject as we understand it today, the most significant being Tseitin's 1968 paper, but none of them introduced general notions that would allow to make an explicit and universal link between lengths-of-proofs problems and computational complexity theory. In this note we shall highlight three particular definitions from the paper: of proof systems, p-simulations and the pigeonhole principle formula, and discuss their role in defining the field. We will also mention some related developments and open problems.