Iowa Type Theory Commute
Iowa Type Theory Commute
Aaron Stump
The proof-theoretic ordinal of Peano Arithmetic is Epsilon-0
14 minutes Posted Dec 11, 2021 at 4:00 am.
0:00
14:10
Download MP3
Show notes

In this episode, I outline the argument for why the proof-theoretic ordinal (in the sense of Rathjen, as presented last episode) is epsilon-0.  My explanation has something of a hole, in explaining how one would go about deriving induction for ordinals strictly less than epsilon-0 in Peano Arithmetic.  To help paper over this hole a little, I discuss a really nice recent exposition of encoding ordinals in Agda.