Commentary by cpressey on Proof Theory works

Basic Proof Theory

.

A Paedagogic Example of Cut-Elimination

The author notes that it was a very deep insight of Gentzen's that classical logic is symmetric between true and false, and this is reflected in the sequent calculus: either what's to left of the turnstile is false, or what's to the right is true.

LI is a cute little theory, but as far as I can tell it's quite weak; the theory of lattices with inequality. Still, it is simple and you can prove some things in it: for example, a weak distributivity law.