Iowa Type Theory Commute

Latest Episodes:

Introduction to Ordinal Analysis Nov 16, 2021

Show notes

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.

An analogy for multiplicative disjunction Nov 03, 2021

Show notes

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.

Linear conjunctions and disjunctions Oct 28, 2021

Show notes

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!

A taste of linear logic Oct 21, 2021

Show notes

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

Structural rules, or the Curse of the Bound Variable Oct 12, 2021

Show notes

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

Why Cut Elimination is More Complicated than Normalization Oct 05, 2021

Show notes

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.

Introduction to Cut Elimination Sep 29, 2021

Show notes

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.

Normalization of detours for implication inferences Sep 19, 2021

Show notes

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

Normalization in natural deduction Sep 18, 2021

Show notes

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 introduction is immediately followed by an elimination.

A Brief Look at Sequent Calculus Sep 15, 2021

Show notes

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 the conclusion of the rule) in the left part of a sequent G => D (i.e., in G), and similarly a right rule for introducing it in the right part (D). The beauty of sequent calculus is disjunction is handled without any departure from the general form for sequent calculus rules (unlike disjunction in natural deduction, as we discussed last time).

Our TOPPODCAST Picks

Follow Us

Stay Connected

Related Podcasts

Links

Stay Connected

Our TOPPODCAST Picks

Follow Us

Stay Connected

Iowa Type Theory Commute

Related Podcasts

1

2

3

4

5

6