形式系统与推理技术.doc

资料内容仅供您学习参考，如有不当或者侵权，请联系改正或者删除。
* 第5章 形式系统与推理技术
读者已经看到, 逻辑代数的确揭示了人类思维的基本规律, 例如┝A∨┐A( 排中律) , ┝ ┐(A∧┐A)( 矛盾律) , A∧(A→B)┝ B( 假言推理) , A→(B∧┐B) ┝ ┐A( 归谬推理) , (A∨B)∧ (A→C)∧(B→C)┝ C( 穷举推理) ; 逻辑代数还提供了真值计算、 代入、 替换、 对偶等演算手段, 可用于对其它思维规律的探求。可是, 这与数理逻辑所追求的形式化、 公理化的目标相去甚远。
20世纪初, 数理逻辑研究的一个重要目的在于建立一个严密的数学体系,来刻划人的思维的规律。这个体系以符号语言来表示; 以若干表示最基本逻辑规律的公式( 永真式) 为基础, 称为公理( axioms) ; 以若干可对公式进行重写的规则( 确保由永真式重写出永真式) , 作为系统内公式变换的依据, 称为推理规则( rules of reference) 。系统内推演的全部依据是符号的形式,而不是别的任何东西, 而且系统能导出且只能导出反映人们思维正确规律的永真式, 进而成为人类进行逻辑推理的一个框架, 它保证在前提正确的条件下, 总得出正确的推理结果。这就是所谓数理逻辑的形式系统。[2]
本章先推出一个经典简明的谓词演算形式系统FC( first order predicate calculus formal system) , 借以介绍形式系统的相关概念。然后较完整地讨论一个相对实用的形式系统——自然推理系统, 也称自然演绎系统( natural deduction system) ,简记为ND。

5.1 谓词演算形式系统FC
5.1.1 FC的基本构成
谓词演算形式系统FC由两个部分组成: 1. 谓词演算形式系统FC的语言部分。2. 谓词演算形式系统FC的理论部分。
1. 谓词演算形式系统FC的语言部分。
FC的符号表:
个体变元 x ,y ,z ,u ,v ,w , …
个体常元 a ,b ,c ,d ,e, …
个体间运算符号( 函数符)
f (n) , g (n) , h (n) ,…
其中n为任一正整数, 表示函数的元数。
谓词符号P (n), Q (n), R (n), S (n), …
其中n为非负整数, 表示谓词的元数。当 n = 0时谓词符退化为一个命题常元。
真值联结词 ┐, →
量词 " (把 $v 看作┐"v┐的缩写)
括号 ( , )
FC的更高一级的语言成分有”个体项”和”公式”。
个体项(terms, 以下简称项)归纳定义如下:
( 1) 个体变元和个体常元是项。
( 2) 对任意正整数n, 如果f (n)为一n元函数符, t1 , … ,tn为项, 那么f (n)(t1,…,tn)也是项。
( 3) 除有限次使用( 1) , ( 2) 条款所确定的符号串外, 没有别的东西是个体项。
合式公式(well found formula, 以下简称公式)归纳定义如下:
( 1) 对任意非负整数n, 如果P (n)为一n元谓词符, t1 , … ,tn为项, 那么P (0)( 命题常元) 和P (n) (t1,…,tn)( n > 0) 是公式。
( 2) 如果A, B为公式, v为任一个体变元, 那么(┐A) , (A→B) , ("vA) (或("vA(v)))均为公式。
( 3) 除有限次使用( 1) ( 2) 条款可确认为公式的符号串外, 没有别的东西是公式。
公式中括号的省略原则同前。约束变元、 自由变元及辖域等概念照旧。今后, 我们常见大写拉丁字母A, B, C, …,表示任意公式, 用A(v)等表示公式A中含有自由变元v; 常见大写希腊字母Γ表示一个公式的集合, Γ能够是空集合; 用Γ; A表示在公式集合Γ中添入公式A, 即ΓÈ{A}。
另外, 我们还需要以下定义:
定义5.1 设v1,…,vn是公式A中的自由变元, 那么公式"v1…"vnA(或"v1…"vnA(v1,…,vn)称为A的全称封闭式( generalization clusure) 。A不含自由变元时, A 的全称封闭式为其自身。
2. 谓词演算形式系统FC的理论部分
FC的公理系统包括以下公理( A, B, C为任意公式) :
A1. A→(B→A)
A2. (A→(B→C))→((A→B)→(A→C))
A3. (┐A→┐B)→(B→A)
A4. "xA(x)→A(t/x)( x为任一变元, t为对x可代入的项) 。
A5. "x (A(x)→B(x))→("xA(x)→"x B(x))( x为任一变元) 。
A6. A→"x A( A中无自由变元x) 。
A7. 以上公式的全称封闭式都是FC的公理。
推理规则: (分离规则)。
A1——A3为命题演算的重言式, 也是谓词演算的永真式。A4——A7是谓词演算的永真式。它们的永真性在第3章和第4章已经得到证实。

5.1.2 系统内的推理: 证明与演绎
定义5.2 公式序列A1,A2,…,Am称为Am的一个证明( proof) , 如果Ai(1≤i≤m)或者是公理, 或者由Aj1…,Ajk(j1,…,jk<i)用推理规则推得。当这样的证明存在时, 称Am为系统的定理( theorems) , 记为├*Am, ( *为所讨论的系统名),或简记为├Am 。
定义5.3设G为一公式集合。公式序列A1,A2,…,Am称为Am的以G为前提的演绎( diduction) , 如果Ai(1≤i≤m)或者是 G 中公式, 或者是公理, 或者由Aj1…,Ajk(j1,…,jk<i)用推理规则导出。当有这样的演绎时, Am称为 G 的演绎结果, 记为 G├*Am, ( *为所讨论的系统名), 或简记为G├Am。称 G 和 G 的成员为Am的前提(hypothesis)。
显然, 证明是演绎在 G 为空集时的特例。注意, ├Am与┝Am是不同的, G├Am与 G┝Am也是不同的, 前者都是指形式系统内的推理关系( 证明与演绎) , 而后者则是指公式的真值特性及真值间的逻辑关系。当然, 它们之间应当是一致的, 这正是我们建立形式系统所想要做到的。
例5.1、 例5.2和例5.3是FC系统内证明和演绎的例子。
例5.1 证明: ├FCA→A
证. 其证明序列是
( 1) (A→((A→A) →A)) →((A→(A→A)) →(A→A)) 公理A2
( 2) A→((A→A) →A) 公理A1
( 3) (A→(A→A))→(A→A) 对(1) (2)用分离规则
( 4) A→(A→A) 公理A1
( 5) A→A 对(3)(4)用分离规则
例5.2证明├Fc┐B→(B→A)。
证. 其证明序列是
( 1) ┐B→(┐A→┐B) 公理A1
( 2) (┐A→┐B)→(B→A) 公理A3
( 3) ((┐A→┐B)→(B→A))→(┐B→((┐A→┐B)→(B→A))) 公理A1
( 4) ┐B→( ( ┐A→┐B) →(B→A)) 对(2)(3)用分离规则
( 5) ( ┐B→( ( ┐A→┐B) →(B→A))) →( ( ┐B→( ┐A→┐B) ) →
( ┐B→(B→A)) ) 公理A2
( 6) ( ┐B→( ┐A→┐B) →( ┐B→(B→A)) 对(4)(5)用分离规则
( 7) ┐B→(B→A) 对(1)(6)用分离规则
例5.3 在FC中对任意公式A, B, C, 证明:
{A, B→(A→C)}├FC B→C
证. 其演绎序列为
( 1) A 前提
( 2) B→(A→C) 前提
( 3) A→(B→A) 公理A1
( 4) B→A 对(1) (3)用分离规则
( 5) (B→(A→C))→((B→A)→(B→C)) 公理A2
( 6) (B→A) →(B→C) 对(2) (5)用分离规则
( 7) B→C 对(4) (6)用分离规则

5.1.3 FC的重要性质
现在我们对FC的重要性质作一些讨论。
定理5.1( 合理性, sondness) 若公式A是系统FC的定理, 则A为永真式。若A是公式集 G 的演绎结果, 那么A是 G 的逻辑结果。即
若├FC A, 则┝ A .
若 G├FC A, 则 G┝ A .
本定理的证明是容易的, 因为
( 1) 易证公理A1, A2, A3, A4, A5, A6, A7是永真的。
( 2) 易证分离规则是”保真”的, 即当A, A→B真时, B亦真。
从而由公理和分离规则逐步导出的公式是永真的; 由 G 中公式、 公理及分离规则导出的公式, 在 G 中公式均真时也真。
合理性定理的逆否命题可表述为
若 G┝ A不成立, 则 G├FC A不成立。
因此, 欲证 G├FC A不成立, 只要找出一个个体域、 一种解释和一种指派, 它满足 G 中的每一公式, 但它却弄假A。也就是说要证明一个由前提集合G推导出结论A的推理是无效的, 只要举出一个反例( 一个个体域、 一种解释和一种指派) , 使得前提成立而结论不成立。
作为合理性定理的自然推论我们有:
定理5.2 FC是一致的, 即没有公式A使得├FC A与├FC┐A同时成立。
证 若不然, 据合理性定理有┝ A和┝ ┐A, 但这是不可能的。
更深入的研究表明, FC还是完备的。
定理5.3 ( 完备性, completeness) 若公式A永真, 则A必为FC的定理; 若公式A是公式集 G 的逻辑结果, 那么A必为 G 的演绎结果。即
若┝ A, 那么 ├FC A .
若 G┝ A, 那么 G├FC A .
本定理的证明是相当复杂的, 略去。
由于 {┐, →}是完备联结词组, 而且由于全称量词 " 能够表示存在量词 $ , 因此所有永真式均可用只含联结词┐, →和全称量词 "的形式来表示, 从这个意义上说, 在FC中能够推出前述系统中的一切永真式。这表明FC是一个成功和简化了的谓词演算形式系统。
关于系统FC的性质还有一些重要定理, 它们被称为导出规则, 能够用来简化系统内的推理。
定理5.4( 演绎定理) 对任意公式集 G 和公式A, B, G├A→B当且仅当
G; A├ B
( 当 G = Æ时, ├A→B当且仅当 {A}├ B)
证. 设G├A→B的演绎序列是
A1, A2, …, An(=A→B)
那么可作出由G ; A推出B的演绎:
A1, A2, …, An(=A→B) , A( 前提) , B( 对An,A用分离规则)
反之, 设G ; A├ B, 其演绎是
A1, A2, …, Am-1 , Am(= B)
对演绎长度归纳证明 G├A→B。
( 1) 若B为公理或 G 中成员, 那么可作出由 G 导出A→B 的演绎如下:
B→(A→B)( 公理A1) , B , A→B( 对前两式用分离规则)
( 2) 若B为Ai ,Aj(=A i→B)用分离规则推得:
由于i < m , j < m, 据归纳假设有 G 导出Ai , Aj的两个演绎, 分别记为
C1, C2, …, Cr (= A→A i)
D1, D2, …, Dl (= A→A j = A→(A i→B ))
用它们我们能够作出 G 导出A→B 的演绎:
C1, C2, …, Cr , D1, D2, …, Dl, (A→(A i→B ) )→((A→A i)→(A→B))( 公理A2) ,
(A→A i)→(A→B)( 对前两式用分离规则) , A→B( 对上式与Cr用分离规则)
定理证毕。
例5.4 证明: 对任意公式A, B, C有
├PC(A→B)→((B→C)→(A→C))
证 根据演绎定理只需证
{(A→B), (B→C),A}├ C
( 1) A→B 前提
( 2) B→C 前提
( 3) A 前提
( 4) B 对( 1) , ( 3) 用分离规则
( 5) C 对( 2) , ( 4) 用分离规则
很明显, 利用演绎定理使证明大大简化。
定理5.5 ( 归谬定理) 对任何公式集 G 和公式A, B ,若
G; A├ ┐B , G; A├ B,
那么 G├ ┐A 。
由A→(B∧┐B) ┝ ┐A( 归谬推理) 和完备性定理, 本定理不难理解。
例5.5 求证: 对任何公式A, 有
├ ┐┐A→A ├ A→ ┐┐A
证 据演绎定理, 为证├ ┐┐A→A, 只需证明{┐┐A }├ A。由于
{┐┐A, ┐A }├ ┐┐A且{┐┐A, ┐A}├ ┐A
因此由归谬定理得{┐┐A }├ A。
由于已证├ ┐┐A→A, 故已有├ ┐┐┐A→┐A。另外, ( ┐┐┐A→┐A) →( A→┐┐A) 为公理A3, 因而可用分离规则得├ A→ ┐┐A 。
定理5.6( 穷举定理) 对任何公式集, 公式A, B, 若G; ┐A├ B, G; A├ B, 则G├ B。
由(A∨B)∧(A→C)∧(B→C)┝ C( 穷举推理) 和完备性定理, 本定理也不难理解。
例5.6对任何公式A, B, C, 求证
├ (A→C)→((B→C)→((┐A→B)→C))
证. 据演绎定理, 只需证{A→C, B→C, ┐A→B}├ C
由于, {A→C, B→C, ┐A→B, A}├ C是显然的, 而且{A→C, B→C, ┐A→B, ┐A }├C也是易证的, 因此由穷举定理即得欲证。
定理5.7 ( 全称引入规则) 对FC中任一公式A, 变元v, 如果├A, 那么├"vA。
证 对A的证明序列长度l归纳。
l=1时A为公理, "vA 为A的一个全称化( 当A中有自由变元v时) , 仍为一公理; 或者"vA 由A及公理A6.A→"vA( 当A中无自由变元v时) 推得。总之此时有├"vA。
设l<k时命题真, 而A的证明序列是A1,A2,…,Ak(=A)。若Ak为公理, 那么同上可证├"vA。若Ak由Ai与Aj(i,j<k)用rmp得出, 那么Aj必为Ai→Ak形。据归纳假设, 可知├"vAi以及├"v(Ai→Ak )。另一方面, 我们有公理
"v(Ai→Ak) →("vAi→"vAk)
由它和"v(Ai→Ak)用rmp推出"vAi→"vAk, 对"vAi→"vAk及"vAi再次使用分离规则即得"vAk(="vA)。
归纳完成, ├A蕴涵├"vA得证。
定理5.7还可推广到演绎上来。
定理5.8 ( 推广的全称引入规则) 对FC的任何公式集G, 公式A以及不在G的任一公式里自由出现的变元v, 如果G├A, 那么 G├"vA。
证明留给读者。需要强调指出的是, 定理中的条件”v不是 G 中任一公式的自由变元”是至关重要的, 缺少这一要求, 命题不能成立。例如我们知道
{y=5}├ y2=25
但无论如何不能认为下式是正确的:
{y=5}├ "y(y2=25)
本定理的数学背景是: 当我们用一组与变元v无关的前提演绎出A(v), 表明我们已对任意的v导出A(v), 因而事实上我们已得到"vA(v)。若 G 中有B(v)含自由变元v, 那么我们是在前提B(v)之下演绎得A(v), 故v并非是任意的, 自然不能因此而得"v A(v) 。
例5.7 对任何公式A, B及任意变元x证明:
"x(A(x)→B(x))→($xA(x)→$x B(x))( $为┐"┐的简记符)
证 据演绎定理只要证
{"x(A(x)→B(x)), $x A(x) }├ $xB(x)
( 1) "x(A(x)→B(x)) 前提
( 2) $x A(x) 前提
( 3) "x(A(x)→B(x))→(A(x)→B(x)) 公理A4
( 4) A(x)→B(x) 对( 1) , ( 3) 用分离规则
( 5) (A(x)→B(x))→(┐B(x)→┐A(x)) 重言式
( 6) ┐B(x)→┐A(x) 对( 4) , ( 5) 用分离规则
( 7) "x(┐B(x)→┐A(x)) 定理5.8
( 8) "x(┐B(x)→┐A(x))→("x┐B(x)→"x┐A(x)) 公理A5
( 9) "x┐B(x)→"x┐A(x) 对( 7) , ( 8) 用分离规则
( 10) ("x┐B(x)→"x┐A(x))→(┐"x┐A(x)→┐"x┐B(x))
公理A3
( 11) ┐"x┐A(x)→┐"x┐B(x) 对( 9) , ( 10) 用分离规则
( 12) $xA(x)→$x B(x) $x是 ┐"x┐的缩写
( 13) $x B(x) 对( 2) , ( 12) 用分离规则
在许多场合下, 使用存在量词是方便的, 对 $ 有下列重要事实。
定理5.9( 存在消除规则) 设A, B为任意公式, 变元x是公式A、 但不是公式B的自由变元, 那么当, ├ $x A(x) , A(x)├ B同时成立时, 应有├ B 。
它也有一个推广形式。
定理5.10( 推广的存在消除规则) 设 G 为一公式集, A, B为任意公式, 变元x是A的自由变元, 但不是 G 中任一公式以及公式B的自由变元那么当 G├ $x A(x) , G È{ A(x) }├ B同时成立时, 应有 G├ B 。
证 由 G È{ A(x) }├ B及演绎定理, 得 G├ A(x)→B。由于 G 中无自由变元x, 据定理5.8有 G├ "x(A(x)→B) 。据例5.7及 G├ "x(A(x)→B), G├ $x A(x) , 可得 G├ $xB。另一方面, 由于B中无自由变元x, ┐B→"x┐B为公理A6, 从而有┐"x┐B→B , 即 $xB→B 。据此与 G├ $x A即得 G├ B 。
本定理之因此称为”存在指定规则”、 ”存在消除规则”, 是因为它能够理解为: 当有了演绎结果 $xA(x)后, 便可将A(x)看作附加的演绎前提( 从而消除了量词) , 当由此推得与x无关的B时, 可确认B为原前提的演绎结果, B不再依赖于A( 仅仅依赖 $xA, 从而仅依赖原前提) 。这就像在数学论证中我们常常做的那样: 当已经知道方程F(x) = 0有根时( 即 $x (F(x)=0)) , 不妨设有根x0, 然后据F(x0) = 0作进一步的推理。如果得出的结论与x0无关, 那么说明所得结论不依赖于”根是什么”, 而仅依赖于”有根”这一事实。这就是说, 这个结论是 $x (F(x)=0)及原前提的演绎结果, ”不妨设F(x0) = 0”的证明过程是合理的。

练习5.1
1、 什么是形式系统的证明和演绎?
2、 在FC中对下列各式给出证明或演绎, 其中A, B, C为任意公式( 允许使用演绎定理和其它导出规则) 。
( 1) ├ (A→B) →((┐A→┐B)→(B→A))
( 2) ├ A→(B→(A→B))
( 3) {A→(A→B) }├ A→B
( 4) {┐A}├ A→B
( 5) {┐┐A}├ A
( 6) {A→B , ┐(B→C) → ┐A } ├ A→C
( 7) ├ A→┐┐A
( 8) ├(B→A)→(┐A→┐B)
( 9) ├ ( (A→B)→ A)→A
( 10) ├ ┐(A→B)→(B→A)
3、 证明关于FC的元定理: 若 G├ ┐A→B, G; A├ C, G; B├ C, 则 G├ C 。
4、 证明: 对任何公式A(x), B(x)有
( 1) ├FC"x(A(x)→(B(x)→A(x)))
( 2) ├FC "x A(x)→$xA(x)
( 3) ├FC ("x┐A(x)→$xB(x))→(┐$xB(x)→$xA(x))
5、 指出下列FC中的演绎里的错误之处:
( 1) $x A(x,y) 前提
( 2) "y $x A(x,y) 对( 1) 用定理 2.5
( 3) "y $x A(x,y)→$x A(x,x) 公理
( 4) $x A(x,x) 对( 2) , ( 3) 用分离规则
6、 模仿定理5.7的证明, 给出定理5.8的证明。

5.2 自然推理形式系统ND
对FC我们没有做过多的系统内部的推演, 因为它过于复杂, 例5.1、 例5.2和例5.3已充分显示出这一点。在FC中推演复杂的原因主要有两个: 一是FC追求简洁, 只用两个联结词、 一个量词和一条推理规则; 二是推理规则与人的日常推理特点没有联系。如果使用五个联结词、 两个量词和多条推理规则, 那么会使系统的描述能力更强、 更自然。另外, 如果模仿人的数学推理的常见手段, 允许在推理中引入假设, 将使得推理更加高效和便捷。人们常见的那些假设包括:
( 1) 为证A→B, 常假设A而去证明B, 如果成功, 则完成了A→B的证明( 证明结果不再依赖假设A) 。
( 2) 为证A, 常假设┐A而去证明可导出矛盾( 假命题f) , 如果成功, 则完成了A的证明( 证明结果不再依赖假设┐A) 。
( 3) 已证( 或已知) A∨B, 欲证C, 常假设A和B分别去证明C, 如果都能成功, 则完成了C的证明( 证明结果不再依赖假设A, 也不依赖假设B) 。
( 4) 已证( 或已知) $vA(v), 常假设A(v0), 去证明C( 它与v0无关) , 如果能成功, 则完成了C的证明( 证明结果不再依赖假设A(v0)) 。
如果说FC是一个研究系统, 那么ND能够说是一个应用系统。为了便于实际应用中对问题的描述, ND采用五个真值联结词; 为了便于推理, ND采用少数公理, 多数规则, 而且把人的推理手段用推理规则加以体现, 因而它被称为自然推理系统( Natural Deduction system) , 简记为ND。

5.2.1 ND的基本构成
自然推理系统ND的语言与FC大同小异, 主要区别是ND中使用五个真值联结词。其推理部分与FC相去甚远。由于强调人的自然推理, ND更注重演绎, 它的公理表示为Γ├ F形, 例如 用Γ; A├A代替A →A; 其推理规则形如

例如用取代分离规则。
ND的理论部分组成如下。
公理模式只有一个
Γ; A├ A
推理规则模式为18个
1、 假设引入规则

它源于重言式B→( A→B) 。规定了假设引入的合理性。
2、 假设消除规则

它源于重言式ØA →( A →B) 上述两条规则反映了人在推理中常见的模式: 分别情
况进行证明。在假设A与ØA后均要导出B, 则B可推得( 不依赖假设A或ØA) 。
3、 ∨引入规则

它们源于重言式A→AVB和B→AVB。它们能够改用更强的形式

这是由于( ØA→B) «A∨B为永真式。在自然推理中人们常见如下方式: ”欲证A∨B, 可设ØA( ØB) 而证B( A) 。
4、 ∨消除规则

这是重言式( A∨B) ∧( A→C) ∧( B→C) →C的演绎表示形式, 它也反映了数学
推理中分别情况进行证明的思想。如果接受Γ├A∨ØA, 那么假设消除规则只是本规则的特例。
5、 ∧引入规则

它依据重言式A →( B →( A∧B) ) 。
6、 ∧消除规则

它们依据重言式A∧B →A, A∧B →B。
7、 →引入规则

此即演绎定理。为证A →B, 人们常以A为假设而证B。
8、 →消除规则

此即分离规则。
9、 Ø引入规则
,
这一规则反映了数学推理的反证法的基本思想。为证ØA, 假设A导出矛盾B∧ØB。容易验证永真式( A →B) ∧( A →ØB) →ØA 。
10、 Ø消除规则

它源于重言式A→( ØA→B) 。
11、 ØØ引入规则

12、 ØØ消除规则

规则11与12源于重言式A«ØØA。
13、 «引入规则

14、 «消除规则

规则13、 14源于重言式( A«B) «( A →B) ∧( B →A) 。
15、 "引入规则
(v在 A 中无自由出现)
(v在 G 中无自由出现)
本规则依据关于FC的公理A6和定理5.8。这一规则反映了数学推理中的下述做法: 为证"vA(v), 只要排除对变元v的任何限定( 即与任一前提无关) , 不失一般性地证明对任意v, A(v)均真。
16、 "消除规则
(t对v可代入)
它依据FC的公理"xA(x)→A(t/x)( x为任一变元, t为对x可代入的项) 。
17、 $引入规则

它依据永真式A(t)®$vA(v/t)( 这里v/t 表示将项t的所有出现改为变元v, t对v可代入) 。
18、 $消除规则

这里e为G及公式A, C中均无出现的常元。它来源于人们在数学中常见的一条引进假设进行推理的规则: 当我们有了$vA(v)后,便可将A(e)看作附加的演绎前提, 当得到与e无关的C时, 可确认C已推出, 即它并不依赖于A而成立。这就象数学证明中我们常做的那样: 当推知方程F(x)=0有根( 即$x(F(x)=0)) 时, 可设这个根为x0( 即F(x0)=0) , 然后再据此去证所需的结论, 只要所证结论与x0的性质( 除x0为F(x)=0的根这一性质) 无关, 它就是有效的演绎结果。

5.2.2 ND的系统内推理及性质
定义5.4 在ND中, 称A为Γ的演绎结果( deductive consequences) ,即Γ├NDA( 以下将ND省略) , 如果存在序列
( Γ=Γ1) Γ1├ A1, Γ2├ A2, …, Γn├ An(Γn =Γ, An =A)
使得Γi├ Ai(1≤i≤n)或者是公理, 或者是Γj├ Aj(j<i), 或者是对Γj1├ Aj1,…, Γjk├ Ajk(j1, …,jk<i)使用推理规则导出的。称A为ND的定理, 如果有Γ├ A且Γ= Æ。
下列例子可说明ND中的推演过程及风格。
例5.8 证明: 对任一ND的公式A, A∨┐A为ND的定理。
( 1) A├A 公理
( 2) A├A∨┐A ∨引入规则( 1)
( 3) ┐A├ ┐A 公理
( 4) ┐A├A∨┐A ∨引入规则( 3)
( 5) ├A∨┐A 假设消除规则( 2) ( 4)
( 这里”某某规则( a1) …( an) ”表示”对( a1) …( an) 诸式用某某规则”, 下同) 。
例5.9 证明: 对ND的任意公式A, B:
( 1) ┐(A∨B)«┐A∧┐B
( 2) ┐(A∧B)«┐A∨┐B (德摩根律)
我们只证( 1) , 把( 2) 的证明留给读者。
( i) ┐(A∨B),A├A 公理
(ii) ┐(A∨B),A├A∨B ∨引入规则( i)
( iii) ┐(A∨B),A├ ┐( A∨B) 公理
( iv) ┐(A∨B)├ ┐A ┐引入规则( ii) ( iii)
( v) ┐(A∨B) ├ ┐B ( 同理)
( vi) ┐(A∨B)├ ┐A∧┐B ∧引入规则(iv)(v)
(vii) ├ ┐(A∨B) →(┐A∧┐B) →引入规则(vi)
(viii) ┐A∧┐B,A∨B,A├A 公理
(ix) ┐A∧┐B,A∨B,A├ ┐A∧┐B 公理
(x) ┐A∧┐B,A∨B,A├ ┐A ∧消除规则(ix)
(xi) ┐A∧┐B,A∨B,A├A∧┐A ∧引入规则(viii)(x)
(xii) ┐A∧┐B,A∨B,B├B (与(viii)同理)
(xiii) ┐A∧┐B,A∨B,B├ ┐B (与(x)同理)
(xiv) ┐A∧┐B,A∨B,B├A∧ ┐A ┐消除规则(xii)(xiii)
(xv) ┐A∧┐B,A∨B├A∨B 公理
(xvi) ┐A∧┐B,A∨B├A∧┐A ∨消除规则(xi)(xiv)(xv)
(xvii) ┐A∧┐B,A∨B├A ∧消除规则(xvi)
(xviii) ┐A∧┐B,A∨B├ ┐A ∧消除规则(xvi)
(xix) ┐A∧┐B├ ┐(A∨B) ┐引入规则(xvii)(xviii)
(xx) ├ (┐A∧┐B) →┐(A∨B) →引入规则(xix)
(xxi)├ ┐(A∨B) «(┐A∧┐B) «引入规则(vii)(xx)
例5.10 证明: 对ND中的任意公式A, B有
ØA→B├A∨B , A∨B├ØA→B
证. 为简化过程缩短篇幅, 对某些步骤作了省略。先证ØA→B├A∨B
( 1) ØA→B, ØA├ B 公理及→消除规则
( 2) ØA→B, ØA├A∨B ∨引入规则( 1)
( 3) ØA→B, A├A∨B 公理及∨引入规则
( 4) ØA→B├A∨ØA 例5.8 ?
( 5) ØA→B├A∨B ∨消除规则( 2) ( 3) ( 4)
再证A∨B├Ø A→B。
( 1) A∨B, B, Ø A├B