第5章 形式系统与推理技术.doc

* 第5章 形式系统与推理技术读者已经看到，逻辑代数的确揭示了人类思维的基本规律，例如AA（排中律）， (AA)（矛盾律），A(AB) B（假言推理），A(BB) A（归谬推理），(AB) (AC)(BC) C（穷举推理）; 逻辑代数还提供了真值计算、代入、替换、对偶等演算手段，可用于对其它思维规律的探求。但是，这与数理逻辑所追求的形式化、公理化的目标相去甚远。 20世纪初，数理逻辑研究的一个重要目的在于建立一个严密的数学体系,来刻划人的思维的规律。这个体系以符号语言来表达；以若干表示最基本逻辑规律的公式（永真式）为基础，称为公理（axioms）；以若干可对公式进行重写的规则（确保由永真式重写出永真式），作为系统内公式变换的依据，称为推理规则（rules of reference）。系统内推演的全部依据是符号的形式,而不是别的任何东西，并且系统能导出且只能导出反映人们思维正确规律的永真式，进而成为人类进行逻辑推理的一个框架，它保证在前提正确的条件下，总得出正确的推理结果。这就是所谓数理逻辑的形式系统。2本章先推出一个经典简明的谓词演算形式系统FC（first order predicate calculus formal system），借以介绍形式系统的相关概念。然后较完整地讨论一个相对实用的形式系统自然推理系统，也称自然演绎系统（natural deduction system）,简记为ND。5.1 谓词演算形式系统FC5.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) , (AB) , (vA) (或(vA(v)均为公式。 （3）除有限次使用（1）（2）条款可确认为公式的符号串外，没有别的东西是公式。公式中括号的省略原则同前。约束变元、自由变元及辖域等概念照旧。今后，我们常用大写拉丁字母A，B，C, ,表示任意公式，用A(v)等表示公式A中含有自由变元v；常用大写希腊字母表示一个公式的集合，可以是空集合；用；A表示在公式集合中添入公式A，即A。此外，我们还需要以下定义：定义5.1 设v1,vn是公式A中的自由变元，那么公式v1vnA(或v1vnA(v1,vn)称为A的全称封闭式（generalization clusure）。A不含自由变元时，A 的全称封闭式为其自身。2. 谓词演算形式系统FC的理论部分 FC的公理系统包括以下公理（A，B，C为任意公式）：A1. A(BA)A2. (A(BC)(AB)(AC)A3. (AB)(BA) A4. xA(x)A(t/x)（x为任一变元，t为对x可代入的项）。 A5. x (A(x)B(x)(xA(x)x B(x)（x为任一变元）。 A6. Ax A（A中无自由变元x）。 A7. 以上公式的全称封闭式都是FC的公理。推理规则: (分离规则)。A1A3为命题演算的重言式，也是谓词演算的永真式。A4A7是谓词演算的永真式。它们的永真性在第3章和第4章已经得到证实。5.1.2 系统内的推理：证明与演绎 定义5.2 公式序列A1,A2,Am称为Am的一个证明（proof），如果Ai(1im)或者是公理，或者由Aj1,Ajk(j1,jki)用推理规则推得。当这样的证明存在时，称Am为系统的定理（theorems），记为*Am, ( *为所讨论的系统名),或简记为Am 。定义5.3设G为一公式集合。公式序列A1,A2,Am称为Am的以G为前提的演绎（diduction），如果Ai(1im)或者是 G 中公式，或者是公理，或者由Aj1,Ajk(j1,jki)用推理规则导出。当有这样的演绎时，Am称为 G 的演绎结果，记为 G*Am, ( *为所讨论的系统名)，或简记为GAm。称 G 和 G 的成员为Am的前提(hypothesis)。显然，证明是演绎在 G 为空集时的特例。注意，Am与Am是不同的，GAm与 GAm也是不同的，前者都是指形式系统内的推理关系（证明与演绎），而后者则是指公式的真值特性及真值间的逻辑关系。当然，它们之间应当是一致的，这正是我们建立形式系统所想要做到的。 例5.1、例5.2和例5.3是FC系统内证明和演绎的例子。 例5.1 证明：FCAA 证. 其证明序列是 （1）(A(AA) A) (A(AA) (AA) 公理A2 （2）A(AA) A) 公理A1（3）(A(AA)(AA) 对(1) (2)用分离规则 （4）A(AA) 公理A1 （5）AA 对(3)(4)用分离规则例5.2证明FcB(BA)。证. 其证明序列是（1）B(AB) 公理A1（2）(AB)(BA) 公理A3（3）(AB)(BA)(B(AB)(BA) 公理A1（4）B（AB）(BA)） 对(2)(3)用分离规则（5）（B（AB）(BA)）（B（AB） （B(BA)） 公理A2（6）（B（AB）（B(BA)） 对(4)(5)用分离规则（7）B(BA) 对(1)(6)用分离规则例5.3 在FC中对任意公式A，B，C，证明： A，B(AC)FC BC证. 其演绎序列为（1）A 前提（2）B(AC) 前提（3）A(BA) 公理A1（4）BA 对(1) (3)用分离规则（5）(B(AC)(BA)(BC) 公理A2（6）(BA) (BC) 对(2) (5)用分离规则（7）BC 对(4) (6)用分离规则5.1.3 FC的重要性质现在我们对FC的重要性质作一些讨论。 定理5.1（合理性，sondness）若公式A是系统FC的定理，则A为永真式。若A是公式集 G 的演绎结果，那么A是 G 的逻辑结果。即 若FC A，则 A . 若 GFC A，则 G A . 本定理的证明是容易的，因为 （1）易证公理A1，A2，A3，A4，A5，A6，A7是永真的。 （2）易证分离规则是“保真”的，即当A，AB真时，B亦真。 从而由公理和分离规则逐步导出的公式是永真的；由 G 中公式、公理及分离规则导出的公式，在 G 中公式均真时也真。 合理性定理的逆否命题可表述为 若 G A不成立，则 GFC A不成立。因此，欲证 GFC A不成立，只要找出一个个体域、一种解释和一种指派，它满足 G 中的每一公式，但它却弄假A。也就是说要证明一个由前提集合G推导出结论A的推理是无效的，只要举出一个反例（一个个体域、一种解释和一种指派），使得前提成立而结论不成立。 作为合理性定理的自然推论我们有: 定理5.2 FC是一致的，即没有公式A使得FC A与FCA同时成立。 证 若不然，据合理性定理有 A和 A，但这是不可能的。 更深入的研究表明，FC还是完备的。 定理5.3 （完备性，completeness）若公式A永真，则A必为FC的定理；若公式A是公式集 G 的逻辑结果，那么A必为 G 的演绎结果。即 若 A，那么 FC A . 若 G A，那么 GFC A . 本定理的证明是相当复杂的，略去。由于 ，是完备联结词组，并且由于全称量词 可以表示存在量词 $ ，因此所有永真式均可用只含联结词，和全称量词 的形式来表示，从这个意义上说，在FC中可以推出前述系统中的一切永真式。这表明FC是一个成功和简化了的谓词演算形式系统。 关于系统FC的性质还有一些重要定理，它们被称为导出规则，可以用来简化系统内的推理。定理5.4（演绎定理）对任意公式集 G 和公式A，B，GAB当且仅当 G；A B（当 G = 时，AB当且仅当 A B）证. 设GAB的演绎序列是 A1, A2, , An(=AB)那么可作出由G ；A推出B的演绎： A1, A2, , An(=AB) ，A（前提），B（对An,A用分离规则） 反之，设G ；A B，其演绎是 A1, A2, , Am-1 , Am(= B)对演绎长度归纳证明 GAB。 （1）若B为公理或 G 中成员，那么可作出由 G 导出AB 的演绎如下： B(AB)（公理A1），B , AB（对前两式用分离规则） （2）若B为Ai ,Aj(=A iB)用分离规则推得：由于i m , j m，据归纳假设有 G 导出Ai , Aj的两个演绎，分别记为 C1, C2, , Cr (= AA i) D1, D2, , Dl (= AA j = A(A iB )用它们我们可以作出 G 导出AB 的演绎： C1, C2, , Cr , D1, D2, , Dl, (A(A iB ) )(AA i)(AB)（公理A2）,(AA i)(AB)（对前两式用分离规则），AB（对上式与Cr用分离规则）定理证毕。 例5.4 证明：对任意公式A，B，C有 PC(AB)(BC)(AC) 证 根据演绎定理只需证 (AB), (BC),A C （1）AB 前提 （2）BC 前提 （3）A 前提 （4）B 对（1），（3）用分离规则 （5）C 对（2），（4）用分离规则 很明显，利用演绎定理使证明大大简化。定理5.5 （归谬定理）对任何公式集 G 和公式A，B ,若G；A B ，G；A B，那么 G A 。由A(BB) A（归谬推理）和完备性定理，本定理不难理解。 例5.5 求证：对任何公式A，有 AA A A证 据演绎定理，为证 AA，只需证明A A。由于A, A A且A, A A因此由归谬定理得A A。由于已证 AA，故已有 AA。此外，（AA）（AA）为公理A3，因而可用分离规则得 A A 。 定理5.6（穷举定理）对任何公式集，公式A，B，若G；A B，G；A B，则G B。由(AB)(AC)(BC) C（穷举推理）和完备性定理，本定理也不难理解。例5.6对任何公式A，B，C，求证 (AC)(BC)(AB)C) 证. 据演绎定理，只需证AC, BC, AB C由于，AC, BC, AB，A C是显然的，而且AC, BC, AB，A C也是易证的，因此由穷举定理即得欲证。定理5.7 （全称引入规则） 对FC中任一公式A，变元v，如果A，那么vA。证 对A的证明序列长度l归纳。l=1时A为公理，vA 为A的一个全称化（当A中有自由变元v时），仍为一公理；或者vA 由A及公理A6.AvA（当A中无自由变元v时）推得。总之此时有vA。设lk时命题真，而A的证明序列是A1,A2,Ak(=A)。若Ak为公理，那么同上可证vA。若Ak由Ai与Aj(i,jk)用rmp得出，那么Aj必为AiAk形。据归纳假设，可知vAi以及v(AiAk )。另一方面，我们有公理 v(AiAk) (vAivAk)由它和v(AiAk)用rmp推出vAivAk，对vAivAk及vAi再次使用分离规则即得vAk(=vA)。归纳完成，A蕴涵vA得证。定理5.7还可推广到演绎上来。定理5.8 （推广的全称引入规则） 对FC的任何公式集G，公式A以及不在G的任一公式里自由出现的变元v，如果GA，那么 GvA。 证明留给读者。需要强调指出的是，定理中的条件“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)(xB(x)xA(x) 公理A5 （9）xB(x)xA(x) 对（7），（8）用分离规则（10）(xB(x)xA(x)(xA(x)xB(x) 公理A3（11）xA(x)xB(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, BxB为公理A6，从而有xBB ，即 $xBB 。据此与 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） (AB) (AB)(BA) （2） A(B(AB) （3）A(AB) AB （4）A AB （5）A A （6）AB , (BC) A AC （7） AA （8）(BA)(AB) （9） ( (AB) A)A （10） (AB)(BA) 3、证明关于FC的元定理：若 G AB，G；A C，G；B C，则 G C 。 4、证明：对任何公式A(x)，B(x)有 （1）FCx(A(x)(B(x)A(x) （2）FC x A(x)$xA(x) （3）FC (xA(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）为证AB，常假设A而去证明B，如果成功，则完成了AB的证明（证明结果不再依赖假设A）。（2）为证A，常假设A而去证明可导出矛盾（假命题f），如果成功，则完成了A的证明（证明结果不再依赖假设A）。（3）已证（或已知）AB，欲证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形，例如 用；AA代替A A；其推理规则形如 例如用取代分离规则。ND的理论部分组成如下。公理模式只有一个 ；A A推理规则模式为18个1、 假设引入规则 它源于重言式B（AB）。规定了假设引入的合理性。2、 假设消除规则 它源于重言式A （A B）上述两条规则反映了人在推理中常用的模式：分别情况进行证明。在假设A与A后均要导出B，则B可推得（不依赖假设A或A）。3、 引入规则 它们源于重言式AAVB和BAVB。它们可以改用更强的形式 这是由于（AB）AB为永真式。在自然推理中人们常用如下方式：“欲证AB，可设A（B）而证B（A）。4、 消除规则 这是重言式（AB）（AC）（BC）C的演绎表示形式，它也反映了数学推理中分别情况进行证明的思想。如果接受AA，那么假设消除规则只是本规则的特例。5、引入规则 它依据重言式A （B （AB）。6、消除规则 它们依据重言式AB A，AB B。7、引入规则 此即演绎定理。为证A B，人们常以A为假设而证B。8、消除规则 此即分离规则。9、引入规则 ，这一规则反映了数学推理的反证法的基本思想。为证A，假设A导出矛盾BB。容易验证永真式（A B）（A B）A 。10、消除规则 它源于重言式A（AB）。11、引入规则 12、消除规则 规则11与12源于重言式AA。13、引入规则 14、消除规则 规则13、14源于重言式（AB）（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(1in)或者是公理，或者是j Aj(ji)，或者是对j1 Aj1, jk Ajk(j1, ,jki)使用推理规则导出的。称A为ND的定理，如果有 A且= 。下列例子可说明ND中的推演过程及风格。例5.8 证明：对任一ND的公式A，AA为ND的定理。（1）AA 公理（2）AAA 引入规则（1）（3）A A 公理（4）AAA 引入规则（3）（5）AA 假设消除规则（2）（4）（这里“某某规则（a1）（an）”表示“对（a1）（an）诸式用某某规则”，下同）。例5.9 证明：对ND的任意公式A，B：（1）(AB)AB（2）(AB)AB (德摩根律)我们只证（1），把（2）的证明留给读者。（i）(AB),AA 公理 (ii) (AB),AAB 引入规则（i）（iii）(AB),A （AB） 公理 （iv）(AB) A 引入规则（ii）（iii）（v）(AB） B （同理）（vi）(AB) AB 引入规则(iv)(v) (vii) (AB) (AB) 引入规则(vi) (viii) AB,AB,AA 公理 (ix) AB,AB,A AB 公理 (x) AB,AB,A A 消除规则(ix) (xi) AB,AB,AAA 引入规则(viii)(x) (xii) AB,AB,BB (与(viii)同理) (xiii) AB,AB,B B (与(x)同理) (xiv) AB,AB,BA A 消除规则(xii)(xiii) (xv) AB,ABAB 公理 (xvi) AB,ABAA 消除规则(xi)(xiv)(xv) (xvii) AB,ABA 消除规则(xvi) (xviii) AB,AB A 消除规则(xvi) (xix) AB (AB) 引入规则(xvii)(xviii) (xx) (AB) (AB) 引入规则(xix)(xxi) (AB) (AB) 引入规则(vii)(xx)例5.10 证明：对ND中的任意公式A，B有 ABAB , ABAB证. 为简化过程缩短篇幅，对某些步骤作了省略。先证ABAB（1）AB，A B 公理及消除规则（2）AB，AAB 引入规则（1）（3）AB， AAB 公理及引入规则（4）ABAA 例5.8 ?（5）ABAB 消除规则（2）（3）（4）再证AB AB。（1）AB，B， AB 公理（2）AB，BAB 引入规则（1）（3）AB，A， AB 公理及消除规则（4）AB，AAB 引入规则（3）（5）ABAB 公理（6）ABAB 消除规则（2）（4）（5）容易证明，FC的公理都是ND的定理。例5.11 对任意公式A,B,C有(1) A(BA)(2) (A(BC)(AB)(AC) (3) (A B)(BA)证（1）（i）A,BA 公理（ii）ABA 引入规则（i）（iii）A（BA） 引入规则（ii）证（2）（i）A(BC)，AB，AA 公理 （ii）A(BC)，AB，AAB 公理 （iii）A(BC)，AB，AA(BC) 公理（iv）A(BC)，AB，AB 消除规则（i）（ii）（v）A(BC)，AB，ABC 消除规则（i）（iii）（vi）A(BC)，AB，AC 消除规则（iv）（v）（vii）(A(BC)(AB)(AC) 引入规则(运用3次)证(3)（i） AB , B , AB 公理 （ii）AB , B , AA 公理 （iii） AB , B , AAB 公理（iv）AB , B , AB 消除规则(ii)(iii)（v）AB , BA 引入规则(i)(iv)（vi）AB , BA 消除规则（v）（vii）(AB)(BA) 引入规则(运用2次)此外，FC的公理A5在ND中可证明如下。例5.12证明v(A(v)B(v) (vA(v)vB(v)证. 其演绎序列如下：（1）v(A(v)B(v), vA(v)vA (v) 公理（2）v(A(v)B(v), vA(v)A(v) 消除规则（1）（3）v(A(v)B(v), vA(v)v (A(v)B(v) 公理（4）v(A(v)B(v), vA(v)A(v)B(v) 消除规则（3）（5）v(A(v)B(v), vA(v)B(v) 消除规则（2）（4）（6）v(A(v)B(v), vA(v)vB(v) 引入规则（5）（7）v(A(v)B(v) vA(v)vB(v) 引入规则（6）（8） v(A(v)B(v) (vA(v)vB(v) 引入规则（7）FC的公理A4由ND的 消除规则保证，FC的公理A6和公理A7由ND的 引入规则保证。因此我们有定理5.11 FC的公理均为ND的定理。定理5.12 FC的定理均为ND的定理。这是因为FC的公理均为ND的定理，FC的分离规则就是ND的消除规则。于是，可以得到结论：定理5.13 ND是合理的、完备的，即对任何ND中公式A， GND A，当且仅当 G A。ND是合理的，它的公理和推理规则的合理性在我们给出系统时都已作出了说明。而ND的完备性可由FC的完备性以及定理5.12直接导出。为了使读者对ND的系统内的推演更加熟悉，我们再介绍一些例子。例5.13证明$vA(v)vA(v)证. 其演绎序列如下：（1）$vA(v),vA(v)$vA(v) 公理（2）$vA(v),vA(v), A(c/v) A(c/v) (c为新常元) 公理（3）$vA(v),vA(v), A(c/v)vA(v) 公理（4）$vA(v),vA(v), A(c/v) A(c/v) 消除规则（3）（5）$vA(v),vA(v), A(c/v)BB(B中c无出现) 消除规则（2）（4）（6）$vA(v),vA(v)BB $消除规则（1）（5）（7）$vA(v),vA(v)B 消除规则（6）（8）$vA(v),vA(v) B 消除规则（7）（9）$vA(v) vA(v) 引入规则（7）（8）（10）$vA(v)vA(v) 引入规则（9）vA(v) $vA(v)的证明留给读者完成。本例可以看作是存在量词 $ 的定义式，也就是说，在ND中用一个量词并无不可。ND中还有以下定理，我们在讨论公式的前束范式时已经运用过它们。定理5.14 设A(v)为ND中公式，那么（1）vA(v)$vA(v)（2）$vA(v)vA(v)证（2）。我们只证vA(v) $vA(v)，另一方向的证明留给读者，（1）式的证明类似，省略。（i）vA(v), $vA(v), A(c/v) A(c/v)（c为新常元） 公理（ii）vA(v), $vA(v), A(c/v) A(c/v) 公理及消除规则（iii）vA(v), $vA(v), A(c/v)BB（B中无c） 消除规则（i）（ii）（iv）vA(v), $vA(v)$vA(v) 公理（v）vA(v), $vA(v)BB $消除规则（iii）（iv）（vi）vA(v), $vA(v)B 消除规则（v）（vii）vA(v), $vA(v) B 消除规则（v）（viii）vA(v) $vA(v) 引入规则（vi）（vii）定理5.15 设A(v)，B为ND中公式，B中无v的自由出现，那么（1）Qv(A(v)B)QvA(v)B（2）Qv(A(v)B)QvA(v)B这里Q为 或 $ 。证 我们只证（1）式中Q为的情况，其余证明读者可仿此完成。（i）v(A(v)B), B, A(v)A(v)B 公理（ii）v(A(v)B), B, A(v)(A(v)B)(A(v) B) 例5.10（iii）v(A(v)B), B, A(v) A(v)B 消除规则（i）（ii）（iv）v(A(v)B), B, A(v)B 消除规则（公理）（iii）（v）v(A(v)B), B, A(v) B 公理（vi）v(A(v)B), B A(v) 引入规则（iv）（v）（vii）v(A(v)B), B A(v) 消除规则（vi