Pavel Pudlák: The journey from Peano Arithmetic to proof complexity

This talk is part of Lectures on Logic and Foundations of Mathematics at Wuhan University starting from September 2020, organized by School of Philosophy at Wuhan University in China.

Lecture Title: The journey from Peano Arithmetic to proof complexity
Speaker: Prof. Pavel Pudlák (Mathematical Institute of the Czech Academy of Sciences, Czech)
Date and Time: 2021-05-18, 16:00-18:00 Beijing Time (UTC 8:00-10:00)
Platform: Zoom
Organizer:
School of Philosophy, Wuhan University
Interlocutor:
Prof. Yue Yang (School of Mathematics, National University of Singapore)
Host: Prof. Yong Cheng (School of Philosophy, Wuhan University)

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 Godel 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.