Proof Mining in Bounded Arithmetic

Explore proof mining techniques in bounded arithmetic through this 44-minute lecture by Amirhossein Akbar Tabatabai, presented as part of the Hausdorff Trimester Program: Types, Sets and Constructions. Delve into the computational content of proofs, examining the canonical algorithm, language complexities, and computational reductions. Investigate the main lemma and theorem, focusing on the computability of characteristic functions. Gain insights into practical applications of these concepts in the field of mathematical logic and theoretical computer science.

Intro
The Computational Content
Proof Mining
The Canonical Algorithm
The language
Complexity Classes
Computational Reductions
The Main Lemma
Computability of Characteristic Functions
The proof of the Main Theorem
Applications II