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.

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

Ordinal analysis is an important branch of proof theory, which seeks to compare, quantitatively, the strengths of different proof systems.  The quantities in question are ordinals, which extend the ordering character of natural numbers into the infinite.  In this episode, I discuss these ideas a bit further, and also review a little the ordinals up to epsilon 0.

Listen in while I have an actual insight on air!  After a week of head scratching, I figure out -- while chattering! -- what I hope is both a correct and intuitive example of multiplicative disjunction.

I explain the basic idea of multiplicative versus additive proof rules, and consider multiplicative conjunction (tensor), addition conjunction (&, "with"), additive disjunction -- but leaving multiplicative disjunction (par) for next time!

We discuss briefly the central ideas of linear logic, where by default assumptions must be used exactly once. 

In this episode I discuss the basic structural rules of weakening, contraction, and exchange, and speculate on their dark origin.

Cut elimination for sequent calculus is more involved that normalization of detours for natural deduction.  There are more cases of cuts that must be transformed than correspond to detours (introductions followed by eliminations).  In this episode, I explain why that is.

We saw in the last few episodes that proofs in natural deduction can be simplified by removing detours, which occur when an introduction inference is immediately followed by an elimination inference on the introduced formula.  What corresponds to this for sequent calculus proofs?  The answer is cut elimination.  This episode describes the cut rule and what is meant by a cut-elimination procedure.  We will talk more about such a procedure in the next episode.

We talk about normalizing detours -- which are when an introduction inference is immediately followed by an elimination inference -- for the implication rules.  Under Curry-Howard, this actually corresponds to beta-reduction, and could make the proof bigger (though less complex in a certain sense).