【学习目标】 　　　通过本章的学习，应达到如下目标： 　　　◇　了解λ-演算的基本概念，语法及其基本性质，清楚λ-演算与形式系统之间的关系； 　　　◇　了解Scott域的概念，序关系的定义方法以及同构和投影的定义，了解Scott域优于其它模型的特点和性质； 　　　◇　了解作为直觉主义逻辑一部分的自然推理系统的基本概念和树形表示法，知道该系统在逻辑上的特点； 　　　◇　了解Gentzen串行演算的概念，基本规则及主要特点，了解直觉主义的串行演算的规律与特点，从而进一步体会串行演算系统的优点； 　　　◇　了解近邻空间的定义以及线性串行演算的规则，从而了解线性逻辑思想、方法、系统特性和主要特点。 【学习指南】 　　　本章介绍了证明论中的逻辑系统，学习时应注意把握以下几点： 　　　◇　首先了解证明论是数理逻辑的一个研究内容，是"两个演算"加"四论"的"四论"之一，在数理逻辑中具有特殊的位置； 　　　◇　从λ-演算入手学习证明论，因为λ-演算可以看作是最简单、最小的一个形式系统，是计算机科学的理论基础之一； 　　　◇　学习Scott域加深对 -演算的认识，了解其作为理论模型的特点和优良性质； 　　　◇　从自然推理系统入手学习理解Gentzen串行演算，从而体会它特有的对称性，表达自然和描述直觉主义系统的简明与清晰； 　　　◇　从Gentzen串行演算自然过渡到线性逻辑，学习时注意它与Gentzen串行演算在规则上的变化，从而深刻体会和理解，在语法上一个推理规则的微小变动都会导致推理系统在语义上、本质上的巨大差异这一重要结论； 　　　◇　本章涉及的是数理结构中相对抽象的内容，理论层次较多，不作为本门课程的基本内容。 【重点和难点】 　　　本章讨论的是证明论中的逻辑系统，涉及数理逻辑中较为抽象的内容，所以学习理解时的难点相对较多。 　　　◇　λ-演算的思想是证明论中最基础的内容，也是学习掌握的重点，它是理解本章后续内容的前提和条件； 　　　◇　Scott域中的序关系及同构和投影的内容是理解该思想的重要环节； 　　　◇　Gentzen串行演算是本章中最为重要的内容，它涵盖了自然推理系统、直觉主义逻辑等多方面内容，并且有作为逻辑系统的许多独特的优点，在学习理解时其规则的表示方法及其与直觉主义逻辑的关系是难点所在； 　　　◇　线性逻辑是本章的又一重点，尽管它与Gentzen串行演算仅有微小的差别，对近邻空间的理解是学习本章的难点。 【预习思考题】　　　 　　　◇　证明论作为数理逻辑的研究内容之一具有哪些重要意义？ 　　　◇　函数式程序设计理论的主要基础和并发程序设计的理论工具被称为什么演算？ 　　　◇　推理规则的微小变化是否会导致推理系统的本质差异？ 　　　◇　直觉主义逻辑与形式系统都有哪些联系？ 　　　◇　自然推理系统、线性逻辑和Gentzen串行演算各是什么关系？