Iowa Type Theory Commute
Iowa Type Theory Commute
Aaron Stump
The proof-theoretic ordinal of a logical theory
12 minutes Posted Nov 21, 2021 at 5:00 am.
0:00
12:14
Download MP3
Show notes

Ordinal analysis seeks to determine the strength of a logical theory by assigning an ordinal to it.  Which one?  In this episode I describe a definition of the proof-theoretic ordinal of a logical theory from a paper by proof theorist Michael Rathjen.  It is basically a measure of how strong an induction principle is derivable in the theory.  (The first parts of the paper are pretty accessible, but the rest gets hard, at least for me.)