【CMU硬核书】数理逻辑与计算，526页pdf

这本关于数学逻辑的新书由Jeremy Avigad从句法的角度全面介绍了该学科的基本结果和方法，强调逻辑是对形式语言和系统及其正确使用的研究。主题包括证明理论、模型理论、可计算性理论和公理基础，并特别强调计算机科学的基础数学逻辑方面，包括演绎系统、构造逻辑、简单类型lambda演算和类型理论基础。清晰和引人入胜，有丰富的例子和练习，它是一个优秀的介绍，为研究生和高级本科生谁对逻辑感兴趣的数学，计算机科学，和哲学，和任何实践逻辑学家的书架宝贵的参考。在短语数理逻辑中，“数学的”一词是模糊的。它可以用来指定所用的方法，这样这个短语就指的是数学中对推理原理的研究。可以对所考虑的推理类型进行划分，因此该短语指的是专门研究数学推理的研究。或者它也可以用来表示目的，因此这个短语指的是着眼于数学应用的逻辑研究。在这本书的标题中，“数学的”一词指的是前两种意思，而不是第三种意思。换句话说，数学逻辑在这里被看作是对数学推理方法的数学研究。这门学科本身就很有趣，而且在数学上也有应用。但它在计算机科学中也有应用，例如，硬件和软件的验证，以及数学推理的机械化。通过提供数学的理想模型，它也可以为数学哲学提供信息。逻辑作为一门学科的区别在于它对语言的关注。主体从正式的表达式开始，这些表达式被认为是我们用来定义对象、声明声明和证明它们的非正式语言的模型。在这一点上，两种截然不同的观点出现了。从语义的角度来看，形式表达式用于描述抽象的数学对象和结构。它们可以用来描述像群、环和场这样的结构类;描述特定结构，如欧几里得平面或实数;或者描述一个特定结构中的关系。从这个角度来看，数学逻辑是一门关于参考、可定义性和真理的科学，它阐明了决定数学语言和它所描述的数学结构之间关系的语义概念。本书采用了更多的句法视角，其中主要的兴趣对象是表达式本身。从这个角度来看，形式语言是用来推理和计算的，我们关心的是规范它们正确使用的规则。我们将使用形式系统来理解数学推理的模式以及数学定义和证明的结构，我们还会对我们能用这些语法表示来做的事情感兴趣。我们不会回避使用语义方法，但我们的目标是使用语义来阐明语法，而不是相反。语法方法之所以有价值，原因有很多。句法的数学理论本身就很有趣，而且信息量大。对语法对象的关注也与计算机科学更加一致，因为这些对象可以表示为数据并通过算法进行操作。最后，还有哲学上的好处。因为有限符号串的一般理论是处理表达式所需要的，句法视角提供了一种研究数学推理的方法——包括无限对象和方法的使用——而不必从一开始就引入强大的数学预设。这本书的另一个显著特点是它对计算的关注。一方面，我们期望数学能给我们一个广泛的概念理解。在这个主题的经验边界上，这有助于组织和解释我们的科学观察，但我们对理解的渴望并不局限于经验现象。另一方面，我们也希望数学能告诉我们如何计算轨迹和概率，这样我们就能做出更好的预测和决定，理性地行动，以实现我们的实际目标。概念理解和计算之间存在着张力:计算是重要的，但我们经常通过抑制计算细节看得更远，推理更有效。