Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Proof Theory

Basic Proof Theory

• rating: TODO

.

A Paedagogic Example of Cut-Elimination

• rating: 1

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.