Graham Leigh: On the Computational Content of Classical Sequent Calculus

Explore the computational aspects of classical sequent calculus in this 35-minute lecture by Graham Leigh, presented as part of the Hausdorff Trimester Program on Types, Sets and Constructions. Delve into the intricate relationship between computational interpretations of classical logic and constructive proofs of Herbrand's Theorem. Examine a language-theoretic representation of Herbrand's Theorem for classical sequent calculus, focusing on higher-order recursion schemes (HORS) that compute Herbrand disjunctions from LK proofs. Discover how this approach offers a modular translation and explicit interpretation of the cut rule as term application. Learn about the novel features of this representation compared to other methods, and gain insights into the compositional extraction of term instantiations resulting from reductive cut-elimination. Follow the lecture's structure, covering topics such as Herbrand's theorem, higher-order recursion schemes, terms and types, non-terminals and their types, production rules, and the main results of this joint work with Bahareh Afshari and Stefan Hetzl.

Intro
Herbrand's theorem
Higher-order recursion schemes
Terms and types
The non-terminals
and their types
Production rules 1
Main result
Production rules II