Podcasts Technology Iowa Type Theory Commute Introduction to Cut Elimination

Introduction to Cut Elimination

Published: Sept. 29, 2021, 5 a.m.

b'

We saw in the last few episodes that proofs in natural deduction can be simplified by removing detours, which occur when an introduction inference is immediately followed by an elimination inference on the introduced formula.\\xa0 What corresponds to this for sequent calculus proofs?\\xa0 The answer is cut elimination.\\xa0 This episode describes the cut rule and what is meant by a cut-elimination procedure.\\xa0 We will talk more about such a procedure in the next episode.

'