"数学的本质就在于一切能证明的都要证明。" 　　--G. Frege 　　本章将介绍 l-演算、自然推理系统、Gentzen 的串形演算、Girard 的线性逻辑、模态逻辑等，以及计算机科学、人工智能密切相关的逻辑系统，从理论上介绍它们的语法和语义。 一、λ-演算 　　λ-演算可以说是最简单、最小的一个形式系统。大约在 1930 年左右，由美国的逻辑学家 Kleen 创建。以后的几十年至今，在欧洲得到广泛的发展。可以说，欧洲的计算机科学是从λ-演算开始的，而现在仍然是欧洲计算机科学的基础，它首先是函词式程序理论的基础，而后，在λ-演算的基础上，发展起来的π-演算、χ-演算，成为近年来的并发程序理论的理论工具之一，许多经典的并发程序模型就是以π-演算为框架的。 　　从语义上来说，在美国著名逻辑学家、计算机理论学家 D. Scott 于1960 创建了 Scott 域作为λ-演算的语义之后，利用他的方法，人们先后建立了相空间、紧邻空间等模型，正是在这些语义中研究λ-演算、直觉主义逻辑、F系统、T系统等形式逻辑系统，才使得1986 年左右线性逻辑得以建立起来。 　　简单地说，λ-演算就是表达"代入"或者"置换"这一数学上、计算机计算中这一最简单的、但又是最普遍的运作的。 　　本节介绍λ-演算的语法及其语法上的一些基本性质。 　　λ- 演算的描述 　　1．字母表 　　2．λ-项 　　3．公式 　　4．理论 λ-演算的公理和规则组成 　　定理8.1.1（不动点定理）对每一个F∈∧, 存在M∈∧ ， 使得 λ│-FM =M。 　　定理8.1.2（Church - Rosser定理） 如果λ│-M=N , 则对某一个Z , λ│- M→Z 并且λ│-N→Z 。 　　该定理有等价定理： 　　定理8.1.3（Diamond Property定理） 如果 M→N1 , M→N2 ，则存在某一 Z, 使得 N1→Z , N2→Z 。