内容超好的逻辑学讲义，来自 openlogicproject。

目前有七本，粗略翻了一下目录，intermediate那本和前面的几本有内容重复的。

一本modal logic，一本non-classical logic，这两本应该不用先开始学。列在最前面的两本是内容比较全面但难度又不高的。

总编Richard Zach是哲学系的，欧美很多逻辑学家不在数学系在哲学系，Dirk van Dalen就是例子，没必要因此觉得教材水平不行，但确实比较浅，比数学系的数理逻辑课要求低。

MGZ三人组的an introduction to proof theory是我会向每一位想了解计算机语言技术（plt）的自学者推荐的书（其中Z就是Zach）。这本书的7成内容让你看懂Gentzen的论文和他在哥德尔第二不完备说算术系统一致性无法在这个系统之内证明之后，找到办法证明算术系统一致性的。该论文留下的Natural Deduction和Sequent Calculus是现代证明论的基石。

openlogic的textbooks对这两个系统都有很好的介绍。这非常好，因为对plt来说，虽然first order logic的model theory，以及λ的model也最好有了解，但proof theory更重要，type，typing rules，typed λ，主要来自proof theory。

我还读过Zach的其它论文，超级棒。我非常喜欢他的写作方式，可能因为他是哲学系而不是数学系的，它在认识论（epistemology）角度对逻辑的解释异常清晰，既不超越符号本身的信息瞎比喻，也不仅仅是blindly manipulating symbols，尤其是一些要做取舍的技术细节他通常会说清楚为什么会选择这个方式，或者为什么后来大多数学者选择了这种技术，等等。这和某些计算机书作者胡咧咧是本质区别。

你可能很难想象逻辑系统不但有非常多的分支，而且有deduction系统的选择；现代逻辑学很容易就reconcile了曾经争议不断的哲学问题，在符号里找出了结构问题，假设的使用问题，泛化出相当万能的deduction系统并仍然能让这些系统保持良好特性，比如cut elimination和normalization，从而让传统逻辑系统都是它的一个fragment。从证明论角度看λ是(proof-) term calculus，未来会有越来越多的「增强型」λ系统（比如λμ）进入（函数式）编程语言的设计和实践中。对logic，deduction有一个solid的理解，是secure未来的。

http://t.cn/A6mYZUKl