Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

YouTube

Graham Leigh: On the Computational Content of Classical Sequent Calculus

Hausdorff Center for Mathematics via YouTube

Overview

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.

Syllabus

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

Taught by

Hausdorff Center for Mathematics

Reviews

Start your review of Graham Leigh: On the Computational Content of Classical Sequent Calculus

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.