Start / Iowa Type Theory Commute / The proof theoretic ordinal of a logical theory

Iowa Type Theory Commute

The proof-theoretic ordinal of a logical theory

12 min • 21 november 2021

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.)

Senaste avsnitt

Correction: the Correct Author of the Proof from Last Episode, and an AI flop

12 maj | 7 min

Krivine's Proof of FD, Using Intersection Types

5 maj | 22 min

A Measure-Based Proof of Finite Developments

16 april | 23 min

Introduction to the Finite Developments Theorem

27 mars | 16 min

Nominal Isabelle/HOL

31 januari | 16 min
Vad är en podd?

En liten tjänst av I'm With Friends. Finns även på engelska.

Podcastbild

00:00 -00:00
00:00 -00:00