"数学的本质就在于一切能证明的都要证明。"
  --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 , λ│- MZ 并且λ│-NZ
  该定理有等价定理:
  定理8.1.3(Diamond Property定理) 如果 M→N1 , M→N2 ,则存在某一 Z, 使得 N1→Z , N2→Z 。