Shuwei Wang (Leeds)

A proof theorist's job, part II: into harmonious systems

This talk will be about ordinal analysis, a technique at the core of a proof theorist's toolchain. Using Tait calculus as the formal proof system for arithmetic, we will replicate Gentzen's famous consistency proof as the seemingly useless statement "enough of set theory ⊢ Con(PA)". Hopefully, I will convince the audience that the left-hand side of the turnstile can be weakened to a theory of transfinite induction formalised in primitive recursive arithmetic, and this proof thus measures the proof-theoretic strength of a formal theory using the linear ordering in a given ordinal representation system.