今年立的旗，an introduction...

今年立的旗，an introduction to proof theory，应该无法全部完成，但已经进度过半，看完cut elimination大定理没有问题，看完算术系统一致性的证明应该也问题不大，但后面两章ordinal analysis十有八九看不懂。

没关系。懂与不懂都是收获。给明年立旗了。这本，明年搞定。这本书是讲type的，也不是面向cs的，是讲怎么在type系统里表达数学的。也因此两大证明器路线，higher order logic，和dependent types/CoC都有讲。hol的书很少，除了这本就只有Peter Andrews的一本逻辑学和类型论「入门」；typed lambda的书也不多，除了这本应该就是Barendregt的一本偏数学的。其它一些都是单一领域的不全面。

++++

为了cs和plt那点屁事儿是不是要看这么多超范围的东西我也回答不上来。但是逻辑/证明论/类型论，如果不含cs的部分学得很扎实，再去看tapl/pfpl/plfa，以及时下流行的用证明器教plt，coq/agda/idris等等，应该底气比较足吧。