This is meant to be a light post, posing a perhaps naive question. One of the hallmarks of computational proof theory is the association between arithmetic theories and complexity classes, in terms of their provably recursive functions. But is there a general rule for identifying the provably recursive functions of a class of induction invariants?
Tag: induction
‘Simple’ proofs of cut-elimination: classical logic
In the last couple years, I have taught cut-elimination several times to research-level students (ESSLLI ’18, LSS ’18, and to PhD students at the University of Birmingham). Every time I am left squirming when I have to deal with the monster in the closet: . Most cut-elimination proofs do something like this: Main induction on…
