Matthias Baaz - Fast Cut Elimination in Intuitionistic Logic

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