The proof-theoretic ordinal of Peano Arithmetic is Epsilon-0
Iowa Type Theory Commute
English - December 11, 2021 04:00 - 14 minutes - 9.77 MB - ★★★★★ - 13 ratingsTechnology Science Mathematics programming languages computational logic type theory proof assistants cedille Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: The proof-theoretic ordinal of a logical theory
Next Episode: Introduction to Interactive Theorem Provers
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.