Explore a lecture on fast cut elimination in intuitionistic logic presented by Matthias Baaz at the Hausdorff Center for Mathematics. Delve into an elementary procedure for eliminating prenex cuts in LJ without v, contrasting it with the non-elementary elimination process in LK without v. Discover how this approach leads to an elementary function F, allowing for the elimination of cuts in LK with n or fewer quantifiers through a bounded number of iterations. Gain insights into this surprising result, which demonstrates that the iteration bound is independent of the number of implications. Enhance your understanding of logic and proof theory in this 37-minute talk, part of the Hausdorff Trimester Program on Types, Sets and Constructions.
Matthias Baaz - Fast Cut Elimination in Intuitionistic Logic
Hausdorff Center for Mathematics via YouTube
Overview
Syllabus
Matthias Baaz: Fast cut elimination in intuitionistic logic
Taught by
Hausdorff Center for Mathematics