View Source Document

cpressey.md

Commentary by cpressey on Proof Theory works

Basic Proof Theory

By all accounts this is an incredibly dull book. If you are looking for complete, rigorously-worked out definitions of the foundations of proof theory, for some purpose where it is important to have a pre-worked-out fully-worked formalism, this could be the book for you. It is a reference manual for proof theory. If you are looking for something which you can gain insight from by reading - this is probably not the book for you.

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.