第1章 绪论
证明论是数理逻辑中研究一般性证明结构的分支. 在数理逻辑中，真正可以称为“逻辑”的部分，是初等逻辑或一阶逻辑. 初等逻辑大致分为句法和语义两个方面. 句法方面研究逻辑系统，进一步发展为证明论. 语义方面研究语言与结构的相互作用，进一步发展为模型论. 句法与语义也是相互作用的，如逻辑系统的可靠性和完全性. 本章介绍公理系统、形式系统及证明论的发展.
1.1 证明的概念
证明是从一些前提出发推导结论的过程. 证明的方式可以是经验的，也可以是先验的. 经验证明通过观察事物而获得支持命题的证据，而先验证明从基本概念和公理出发通过演绎推理获得真命题. 在欧几里得几何中，每个公理是由基本概念组成的真命题. 从公理出发通过演绎证明定理.
例1.1 三角形内角之和等于180°
证明 设一个三角形的三个内角分别是A，B，C. 延长线段AC和BC，从其交点(角C的顶点)作一条与AB平行的直线.
角C与C′是对顶角. 角A与A′位于平行线同侧，角B与B′位于平行线同侧.所以A=A′并且B=B′. 由于A′+B′+C′=180°，所以A+B+C=180
这个证明使用了以下公理:(I)给定线段可无限延长;(II)过直线外一点可作一条直线与已知直线平行;(III)对顶角相等;(IV)如果一条线与两条平行线相交，那么同侧角相等. 这里(I)和(II)是构造性公理，(III)和(IV)是关于基本概念的公理. 通过对以上证明进行分析，可以看到它首先运用公理(III)和(IV)进行辅助构造，然后运用(I)和(II)及平角的定义，从A′ + B′ + C′=180. 运用等量替换原理得到A + B + C=180 所谓等量替换原理是指，与同一事物相等的任何两个事物彼此相等. 这条原理在欧几里得几何中也可以看作公理.
在很长一段时间内，几何定理证明是演绎推理的范例. 然而，关于证明本身的研究，或者提出一种关于证明的理论，是逻辑学的事情. 亚里士多德创立的逻辑学说，建立了以三段论为核心的逻辑理论. “三段论”这个词是Syllogismos的翻译(希腊语 σνλλoγισμós)，字面意思是由三个命题组成的推理，例如:
命题(A)称为大前提，命题(B)称为小前提，命题(C)称为结论，横线表示“推
出”或“所以”. 然而Syllogismos的基本含义是“计算”或“推理”，翻译为“三
段论”比较形象. 亚里士多德关于推理的说明如下:
一个推理是一个论证，在这个论证中，有些东西被规定下来，由此必然地得出一些与此不同的东西.(Aristotle，1971: 100 a 25-27)
从一些前提A1， ，An必然地得出结论B，这个过程就是推理. 如果B是从A1， ，An必然地得出的，可以写成A1， ，An？B. 在《后分析篇》中，亚里士多德认为，一门演绎科学的基础是基本概念和基本原理. 从基本概念可以定义导出概念，从基本原理(公理)可以证明定理.
亚里士多德的三段论有其自身的句法. 基本命题形式是“S是P”，其中S和P是词项变元，可以用其他字母代替，S称为主项，P称为谓项. 这种形式的命题称为肯定命题. 加上否定词，得到“S不是P”，称为否定命题. 加上量词“所有”和“有的”，组合得到四种命题形式:
(SAP)所有S是P(全称肯定命题)
(SEP)所有S不是P(全称否定命题)
(SIP)有的S是P(特称肯定命题)
(SOP)有的S不是P(特称否定命题)
三段论至少是三个命题之间的推理关系. 在主项S和谓项P的基础上，引入词项变元M(称为“中项”)，就可以得到四个格:
在空位“.”处补充A，E，I，O，就可以得到 256 个不同的式，其中只有 24 个是有效的. 这 24 个有效式列举如下:
这里“有限制的有效式”是指主项非空假设下的有效式. 有效式可以作为规则在推理中使用. 运用这些规则，可以证明一些正确的推理形式. 例如，SAM，MAQ，QEP . SEP，证明如下:
关于三段论也可以用现代逻辑的公理化方法进行研究. 例如，
我们把由公理SAS和规则B组成的系统记为B. 在这个公理系统中，可以证明一些定理. 例如，aAb，qAa，bAd，cAd，aAq证明如下:
如果让变元a，b，c等取值为平面上的点，而aAb解释为“a通达b”，那么系统B就可以看作关于平面上路径的简单推理系统.
1.2 公理系统与形式系统
在一门科学中，一些概念是不加定义的基本概念，通过定义得到的概念称为导出概念. 导出概念都可以还原为基本概念. 在集合论中“属于关系”是不加定义的基本概念，“x ∈ y”是基本表达式; “包含关系”是从基本概念出发定义的概念，“x . y”定义为“对所有集合z，如果z ∈ x，那么z ∈ y”. 并非所有真命题都能证明，无须证明的真命题称为公理，它们的真是自明的. 从公理出发证明的命题称为定理. 由基本概念、导出概念、公理和定理组成的体系称为公理系统.在 19 世纪数学中，出现了各种适用于不同对象的公理系统.
定义 1.1 一个群是结构(G，.，e)，其中G是非空集，. 是G上的二元运算，e ∈ G是常量，并且满足以下公理:
(G1)对任意x，y，z ∈ G都有x .(y？z)=(x？y). z.
(G2)对任意x ∈ G都有x？e=x=e？x.
(G3)对任意x ∈ G存在y ∈ G使得x？y=e.
无论G中元素是什么，只要满足这些公理，就称为一个群. 例如，(Z，+，0)和(Q，+，0)是群，其中Z是整数集，Q是有理数集. 然而(N，+，0)不是群，其中N是自然数集，它违反公理(G3). 群论中从(G1)，(G2)和(G3)出发可以证明定理.
定理 1.1 对任意x ∈ G存在y ∈ G使得y？x=e.
证明 设x ∈ G. 由(G3)得，存在y ∈ G使得x？y=e. 对该元素y，由(G3)得，存在z ∈ G使得y？z=e. 然后推导如下:
所以y？x=e. 这里等式替换规则是，对任意多项式a，b，c，如果a=b，那么用a替换c中b的一次或多次出现得到的结果与c相等.
在符号代数中公理系统为现代逻辑的发展提供了公理化方法. 公理系统中定理证明的过程实质上就是一种演算. 布尔(George Boole，1815～1864)在 1847 年发表的著作《逻辑的数学分析》就是要发展关于演绎推理的演算. 布尔写道: “熟悉当前符号代数理论的人都清楚，分析过程的有效性不依赖于对其中所运用符号的解释，只依赖于符号组合的规律.”(Boole，1847: 1). 布尔试图运用代数方法来研究逻辑推理中的符号组合规律. 布尔认为，“根据真正的分类原则，我们应该不把逻辑与形而上学联系在一起，而是要把逻辑与数学联系在一起.”(Boole，1847:13)在布尔看来，亚里士多德三段论的典型形式确实是符号性的，但这些符号并不像数学符号那样完善. 布尔对演绎推理进行数学分析，重新建立逻辑规则的符号表示. 皮尔士(Charles S. Peirce，1839～1914)不断改进布尔的逻辑代数，1880 年提出相对于布尔代数完全的演绎系统. 皮亚诺(Giuseppe Peano，1858～1932)也研究了算术中的逻辑推理.
弗雷格(Gottlob Frege，1848～1925)在 1879 年的著作《概念文字》中说，“我们把所有需要说明正当理由的真命题分为两类: 一类是纯粹通过逻辑来证明的真命题，另一类是必须得到经验事实支持的真命题.”(Frege，1967: 1)为说明算术判断属于哪一类，弗雷格试图研究凭借逻辑在算术中可以推进到什么程度. 在这个目标指引下，弗雷格提出模仿算术中公式语言构造纯思维的形式语言，称为概念文字. 弗雷格首先引入判断符号 ，它表示断定横线后的内容是真的. 如果没有竖线，则 表示后面的内容而不作判断. 然后弗雷格引入系列符号:
(1)条件: 如果A，那么B.
(2)否定: 并非A.
(3)相等: A与B相等
(4)函数: Φ(A)和 Ψ(A，B)分别表示A的函数 Φ 以及A和B的函数 Ψ. 因此 Φ(A)表示“A有性质 Φ”，而 Ψ(A，B)表示“B与A有 Ψ 关系”.
(5)普遍性: 所有a有性质 Φ.
在线性符号中，条件记为A → B，否定记为 .A，普遍性记为 .aΦ(a). 从基本符号可得到无穷多的符号组合. 例如，线性式 .(A → .(B → .C))可写成:
三段论中四种基本句子形式SAP，SEP，SIP和SOP分别可以写成:
弗雷格进一步给出了九条公理，根据规则可以得到所有的逻辑规律. 例如:
弗雷格认为，逻辑是关于真之一般规律的科学. 公理是逻辑真句子，规则保持逻辑真，因而全部定理是逻辑真句子. 弗雷格的系统本质上是形式化公理系统.
从句子形式方面研究公理和定理，称为公理系统的句法. 为了从句法上研究公理系统，可以引入形式系统的概念. 一个形式系统F是公理系统的形式部分，它由形式语言、公理和推理规则三部分组成. 为了确定形式语言，首先要给出一些基本符号，有穷多个符号组成的符号串是该语言的表达式，按照一定规则形成的有意义的表达式称为公式. 选择一些公式作为形式系统F的公理，再加上一些由前提和结论组成的推理规则，就可以得到形式系统F的定理.
罗素(Bertrand Russell，1872～1970)和怀特海(Alfred Whitehead，1861～1947)的著作《数学原理》采用了皮亚诺的记号和形式规则，表述了形式系统. 然而，这部著作没有把纯逻辑与数学区分开. 1928 年，希尔伯特(David Hilbert，1862～1943)和阿克曼(Wilhelm Ackermann，1896～1962)的著作《数理逻辑原理》清晰表述了谓词逻辑的形式系统，命题逻辑系统是完全的，但谓词逻辑系统的完全性被当作没有解决的问题提出. 1929 年，哥德尔(Kurt G.del，1906～1978)证明了谓词逻辑系统的完全性. 丘奇(Alonzo Church，1903～1995)1936 年证明了谓词逻辑的不可判定性. 数理逻辑形式系统的建立和发展，标志着逻辑学作为一门科学建立起来.
形式系统提供了研究证明的严格方法. 这一方法的发展与希尔伯特提出的数学基础问题密切相关. 希尔伯特在 1921 年提出形式主义纲领，其目标是得到全部数学的形式化公理系统，还要证明系统的一致性. 希尔伯特认为，严格发展任何一门科学的正确方法就是公理化方法. 公理系统的建立要独立于直观，给出的公理要有助于分析基本概念和公理之间的逻辑联系. 建立公理系统之后，一个重要问题就是系统的一致性. 在 20 世纪 20 年代后期，希尔伯特学派对算术系统的元数学问题进行了研究，尝试提出解决数学系统的一致性问题的方法. 哥德尔 1930 年证明了初等算术不可能有完全的形式系统，也不可能通过有穷方法证明算术的一致性. 哥德尔不完全性定理否认了希尔伯特纲领的可行性.
展开
