Abstract:

Proof complexity is a fast growing field connected to logic, computational complexity, and combinatrorial optimization. In order to fully understand the concepts and their importance, one should go to the roots of this field and follow its history. It started with investigations of the Hilbert school at the beginning of the 20th century, whose aim was to prove consistency and completeness of basic theories used in the foundations of mathematics. After the groundbreaking result of Goedel in the 1930s, the incompleteness of Peano Arithmetic and any theory extending it, the focus turned to the study of fragments of Peano Arithmetic. With the advent of computational complexity theory in the 1970s, connections between weak fragments and complexity classes were discovered. Soon after that provability of certain sentences in weak fragments was connected with the existence of polynomial length propositional proofs of sequences of tautologies expressing these sentences in propositional logic. Another boost for the emerging field of proof complexity came from the realization that several heuristic used in combinatorial optimization could be viewed as propositional proof systems.

In this lecture we will briefly review the history and introduce basic concepts of proof complexity. After that we will demonstrate on a concrete example how one can prove an independence result using propositional proof complexity.