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

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

We talk about normalizing detours -- which are when an introduction inference is immediately followed by an elimination inference -- for the implicati...

This episode explains the idea of normalization of proofs in natural deduction.  We want to eliminate so-called detours in proofs, which occur when an...

Sequent calculus is a different style in which proof systems can be formulated, where for each connective, we have a left rule for introducing it (in ...

We discuss the problem of the or-elimination rule in natural deduction, which does not have the correct form for natural deduction inferences.  It is ...

We discuss the problem of the or-elimination rule in natural deduction, which does not have the correct form for natural deduction inferences.  It is ...

This episode begins the discussion of the style of proof known as Natural Deduction, invented by Gerhard Gentzen, a student of Hermann Weyl, himself a...

We continue our gradual entry into proof theory by talking about reflecting meta-logical reasoning into logical rules, and naming the three basic proo...