Shuwei Wang (Leeds)
- Date
- Friday 24 March 2023, 1.00 PM
- Location
- MALL
- Category
- Postgraduate Logic Seminar
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.