git @ Cat's Eye Technologies The-Glosscubator / master by-topic / Proof Theory / commentary / cpressey.md
master

Tree @master (Download .tar.gz)

cpressey.md @masterview markup · raw · history · blame

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.