2．1 推理有效性与命题演算
逻辑研究的目的是分析一个推理的有效性及其根据，我们以上讨论八个基本的有效推理式则是为了分析复合命题构成的推理的有效性及其根据。
对于简单的由复合命题推理，我们可以直接根据这些基本有效式来判定推理是否有效，并说明理由。例如，如下推理
“如果是犯罪嫌疑人，那么必有犯罪动机。王武有犯罪动机。所以王武是犯罪嫌疑人。”
这个推理是无效的。因为它的两个前提一个是蕴涵式，一个是对蕴涵式后件的肯定。而以蕴涵式为前提的推理只能通过肯定前件或否定后件而推出结论，即只有分离式（MP）和逆分离式（MT）两种有效式。肯定蕴涵式的后件，其前件是真假不定的。
但是对于复杂的推理这样做就不够了。例如，下列推理：
如果商品短缺日益严重，那么物价会上涨。如果存在生产过剩，那么物价不会上涨。如果存在通货膨胀威胁，那么财政控制将继续。如果政府改组，那么财政控制将取消。或者存在生产过剩，或者政府改组。因此，商品短缺不会日益严重，或者不再存在通货膨胀威胁。
仅仅孤立地运用八个有效式不可能对这个复杂推理的有效性及其根据做出说明。
虽然孤立地运用八条有效推理式不能证明复杂推理，但它们却提供了证明有效性的基本依据。我们只须以这些有效推理式为基础，增添新的规则和具体行为方法，就可得到一个证明系统。对于任意一个由复合命题构成的推理，只要它是有效的，其有效性就能在这个系统中得到证明。
推理的有效无效是由形式决定的，分析证明复合命题推理的有效性只能从形式方面入手。因此，在系统中证明推理的有效性纯粹是从形式上证明由前提到结论的推演关系。这样描述的推演关系就是一种数学意义上的演算关系。因此这样的系统被称作命题演算系统。
建立命题演算系统有两种方法，一是公理化方法，一是自然演绎方法。公理化的命题演算系统是在形式语言基础上增添公理和变形规则建构起来的。公理是推演的出发点，由公理根据变形规则推演出的是定理。显然，在公理化的系统中，所有定理的可靠性都依赖于公理。这也使得公理化方法离我们的日常思维比较远，因为我们证明一个命题的可靠性并不需要追溯其出发点，往往是只需考虑给定前提的情况。自然演绎方法恰好符合人们日常思维的这一特点。
自然演绎系统与公理系统不同，它没有公理，只有一系列推理规则。它引入特定前提为假设，根据推理规则推演出结论而建构起来的演算系统。由于这个系统描述的推演关系比较直接而自然地反映了人们的思维过程，因而被称作自然演绎系统。我们将以自然演绎系统为基础讨论有效推理的证明。
不过须要说明，我们对自然演绎系统的讨论是以有利于读者理解和运用为目的的，因此在规则的选择和引入顺序上并不太严格。
2．2 有效推理的形式证明
在命题演算系统中对推理有效性的证明称作形式证明。现在我们给出自然演绎系统中形式证明的定义：
形式证明的定义 一个形式证明是一个命题公式序列A1，A2，…，An。其中的任一Ai（1≤i≤n）或者是前提，或者是由前面的公式根据推理规则得到的。序列的最后一个公式An恰好是结论。
自然演绎系统形式证明是建立在推理规则基础之上的。这些规则大约可分为四部分：一、基本推导规则，二、等值替换规则，三、条件证明规则和四、间接证明规则。基本推导规则由上一节讨论的八个有效推理式构成。
一、基本推导规则
1、 组合规则（∧+）
p
q
∴ p∧q
2、 简化规则（∧-）
p∧q
∴ p
3、 假言三段论（∨-）
p∨q
? p
∴ q
4、 附加规则（∨+）
p
∴ p∨q
5、 分离规则（MP）
p→q
p
∴ q
6、 逆分离规则（MT）
p→q
?q
∴ ?p
7、 假言三段论（HS）
p→q
q→r
∴ p→r
8、 二难推理（CD）
(p→q)∧(r→s)
p∨r
∴ q ∨ s
仍以上面的讨论的推理为例讨论如何运用规则建立形式证明。
例1 如果商品短缺日益严重，那么物价会上涨。如果存在生产过剩，那么物价不会上涨。如果存在通货膨胀威胁，那么财政控制将继续。如果政府改组，那么财政控制将取消。或者存在生产过剩，或者政府改组。因此，商品短缺不会日益严重，或者不再存在通货膨胀威胁。
解：设“商品短缺日益严重”为A，“物价会上涨”为B，“存在生产过剩”为C，“存在通货膨胀威胁”为D，“财政控制将继续”为E，“政府改组”为F。
首先将该推理形式化，在此基础上建立该推理有效性的形式证明。
① A → B P
② C → ?B P
③ D → E P
④ F → ? E P
⑤ C ∨ F P / ∴ ?A∨?D
⑥（C →?B）∧（F → ? E） ②④∧+
⑦ ?B ∨? E ⑥⑤CD
⑧（A → B）∧（D → E） ②④∧+
⑨ ?A∨?D ⑦⑧CD
我们看到，这个形式证明是由九个命题公式构成的。其中的前五个是前提，后四个是由前面的公式根据推理规则得到的。例如，第⑥个公式是由前面的第②和第④个公式根据组合规则“∧+”得到的。最后一个即第⑨个公式恰好就是结论。
这个推理显然是有效的，因为基本推导规则的运用保证了由真前提只能推出真结论，即前提真时结论必真，不可能由真前提推出假结论。
我们还看到，整个形式证明的内容可分为三部分：第一部分是序号，它既标示了命题公式出现的顺序，这些序号同时又是在它后面出现的那个公式的代表。第二部分是若干个命题公式，它们或者是前提，或者是由前面的公式根据推理规则得到的。第三部分则是一些根据，它说明每个命题公式在为什么在形式证明中出现。形式证明的这三个构成部分缺一不可。
2．3 等值替换规则
不过，仅有八条基本推导规则还不够，还不足以建立所有推理有效性的形式证明。例如如下推理：
（A∨B）→ C \ ∴ A → C
显然，运用八条基本推导规则不能建立有关这个推理的形式证明。因此我们还需要新的推理规则，这就是等值替换规则。
等值替换规则实际上就是引入一些逻辑等值式作为推理规则，并规定在形式证明中，等值式两边的公式可以相互替换使用。这些规则引入的序号接着基本推导规则编制。
基本推导规则
9、交换律（COM）
(p∧q) ? (q∧p)
(p∨q) ? (q∨p)
10、结合律（Ass）
((p∧q)∧r) ? (p∧(q∧r))
((p∧q)∧r) ? (p∧(q∧r))
11、德摩根律 （DeM）
? (p∧q) ? (?p∨?q)
? (p∨q) ? (?p∧?q)
12、分配律（Dist）
(p∧(q∨r)) ? ((p∧q)∨(p∧r))
(p∨(q∧r)) ? ((p∨q)∧(p∨r))
13、实质蕴涵（Impl）
(p→q) ? (?p∨q)
14、假言易位（Tran）
(p→q) ? (?q →?p)
15、移出律 （Esp）
((p∧q)→r) ? (p→(q→r))
16、实质等值（Equi）
(p?q) ? ((p→q) ∧ (q→p))
17、双否律 （DN）
p ? p
18、重言律 （Taut）
p ? (p∧p)
p ? (p∨p)
在基本推导规则基础上增添等值替换规则，一般的有效复杂推理都能为其建立形式证明。承前例：
例2 （A∨B）→ C \ ∴ A → C
解： ①（A∨B）→ C P \ ∴ A → C
② ?（A∨B）∨ C ①Impl
③ (?A∧?B)∨C ②DeM
④ (?A∨C) ∧ (?B∨C) ③Dist
⑤ ?A∨C ④∧-
⑥ A→C ⑤Impl
再举一例。
例3 如果他主张减轻农民的税负，他将赢得农民的支持。如果他主张政府增加对社会福利的投入，他将赢得工人的支持。如果他既赢得农民的支持又赢得工人的支持，他就肯定能当选。但是他没有当选。所以，或者他不主张减轻农民的税负，或者不主张政府增加对社会福利的投入。
解：设“他主张减轻农民的税负”为A，“他将赢得农民的支持”为B，“他主张政府增加对社会福利的投入”为C，“他将赢得工人的支持”为D，“他肯定能当选”为E。
将推理形式化并建立推理有效性的形式证明：
① A→B P
② C→D P
③ （B∧D）→ E P
④ ?E P \ ∴ ?A∨?C
⑤ ?（B∧D） ③④MT
⑥ ?B∨?D ⑤DeM
⑦ （A→B）∧（C→D） ①②∧+
⑧ （?B→?A）∧(?D→?C) ⑦Tran
⑨ ?A∨?C ⑥⑧CD
运用等值替换规则和基本推导规则必须注意两类规则之间的区别。
等值替换规则是用逻辑等值的命题去代换原命题，无论怎样替换都不改变原命题公式逻辑值。因此，等值替换可以随时进行。例如下列推理：
①（A→B）∧C
② (?A∨B) ∧C ①Impl
③ (?A∧C) ∨(?B∧C) ②Dist
它的公式②源自于对公式的①一个子公式“A→B”运用实质蕴涵Impl规则，公式③则源自于对公式②的整体运用分配律Dist。这意味着等值替换规则既可以对公式的整体，也可以对公式的一部分运用，因为逻辑等值命题相互替换，从真命题只能推出真命题，推理总是有效。
但基本推导规则不同。基本推导规则的运用实际上是一种代入，即用任意命题代换推理式中的命题变元。代入必须处处进行才能保证推理的有效性。例如，如下推理
①（A∧B）→（C∨E）
② A∧B
∴ C∨E ①②MT
该推理是用“A∧B”代换p，“C∨E”代换q，根据分离规则（MP）“p →q，p ? q”得到的。在分离规则MT中p和q各出现了两次，在推理中p和q的每一次出现都是用相同的命题去代换的。因此推理是有效的。
由于基本推导规则的运用是代入，代入必须处处进行，这就决定了基本推导规则只能对公式的整体起作用。试分析如下推理：
① （A∧B）→C
② A \ ∴ C
* ③ A → C ①∧-
④ C ②③MP
当我们设A为真，B、C为假时，该推理的两个前提“（A∧B）→C”和“A”都为真，而结论“C”假。既然存在代换例示使得该推理式的前提真而结论假，这个推理是无效的。因此，这个形式证明一定是错误的。仔细分析我们看到，错误出在公式③，③是由①使用简化规则∧-得到的。然而∧-规则只适用于合取式，而公式①是一个蕴涵式，尽管该公式的前件是合取式，但作为基本推导规则，∧-必须施用于整个公式，而不是公式的一部分。由于第③步错了，整个形式证明因此都是错的。
2．4 条件证明规则C.P
有了基本推导规则和等值替换规则还不足以为所有有效的复杂推理建立形式证明，例如下列推理
A→（B→C） \ ∴ （A→B）→（A→C）
这个推理是有效的，但要证明其有效性还需要引入新的推理规则。因此我们引入条件证明规则C.P。引入这条规则还有一个作用，我们可以简化证明过程。
首先讨论条件证明规则的根据。
有效推理的逻辑特征是：前提真时结论必真，不存在有使其前提真而结论假的例示。如果我们以有效推理的前提的合取为前件，结论为后件构造一个蕴涵式，那么这个蕴涵式就不可能前件真而后件假，即它一定是恒为真，一定是个重言式。相反，如果推理式不是有效的，那么存在这样的例示使得该推理式前提真而结论假。因此，与这个推理式相应的蕴涵式就不可能是重言式。
由此我们看到，如果用一个推理式前提的合取为前件，结论为后件构造一个蕴涵式，那么这个推理式与该蕴涵式之间存在这样一种等价关系：如果推理式是有效的，那么蕴涵式是重言式；如果推理式不是有效的，那么蕴涵式就不是重言式。
等值替换规则中的移出律Exp指出，如下两个蕴涵式是逻辑等值的：
((p∧q)→r) ? (p→(q→r))
两个蕴涵式分别对应于如下推理式
(p∧q)→r 对应于 p→(q→r) 对应于
p p
? ?
? ?
? ?
q ∴ q→r
∴ r
这两个推理式的区别在于：命题公式“q”在左边的推理式中是前提，而在边的推理式中是结论的构成部分。就是说，右边的推理式比左边的少了一个前提“q”，并且它们有不同的结论：左边推理式的结论是“r”，右边推理式的则是“q→r”，“q”从前提中消去而变成了结论的前件。
由于两个蕴涵式是逻辑等值的，即如果一个是重言式，另一个也必是；一个不是重言式，另一个也必不是。因此这两个推理式是等价的：如果一个推理式有效，另一必有效；一个是无效的，另一个也必无效。
由此，我们得到了条件证明规则C?P：
19、条件证明规则C.P
p
?
?
q
∴p→q
仍以上述推理为例讨论条件证明规则的运用。
例4 A→（B→C） \ ∴ （A→B）→（A→C）
解：① A→（B→C） P
② （A∧B）→C ① Exp
③ （B∧A）→C ② Com
④ B→（A→C） ③ Exp
⑤ A→B
⑥ A→（A→C） ④⑤ HS
⑦（A∧A）→C ⑥ Exp
⑧A→C ⑦ Taut
⑨（A→B）→（A→C）⑤-⑧ C?P
由例4我们看到，第⑤步是将结论的前提作为一个附加前提引入了形式证明中，到第⑧步推出了结论的后件，于是就运用C?P规则消去⑤这个附加前提，即以⑤为前件⑧为后件而得到⑨，⑨恰好是结论。
我们在引入附加前提⑤的同时就用线断标明了这个附加前提的辖域。在辖域中出现的⑥、⑦和⑧这几个公式依赖于①和⑤这两个前提。而公式⑨出现在附加前提⑤的辖域之外，因为C?P规则的运用已经将⑤从前提中消去。⑨就只依赖于前提①了。
因此，标明辖域在条件证明规则C?P的运用中有很重要的意义。我们规定，凡引入附加前提必须标明该前提的辖域。而辖域没有封闭，证明就不能结束，因为这时推演出的公式还依赖于附加前提，即依赖于给定前提之外的东西。如果辖域已经封闭，那么在辖域中出现的公式不能再作为推演的根据，因为我们必须保证推出的结论只依赖于给定的前提，不需要除前提外的其它东西。因此，如下形式证明是错误的：
① V∨?U P
② U∨W P
③ （?V∧?X）→?W P \ ∴ ?V→X
④ ?V
⑤ ?U ①④∨-
⑥ W ②⑤∨-
⑦ ?（?V∧?X） ③⑥MT
⑧ V ∨ X ⑦DeM
⑨ ?V→X ⑧ Impl
这个形式证明的错误在于附加前提④的辖域没有封闭。虽然公式⑨与结论有完全相同的形式，但它是出现在附加前提④的辖域内，除给定前提①②③外，它还依赖于④，而④是原前提中没有的。
显然，如果要把结论的一部分作为附加前提引入证明，那么结论应该是形式为蕴涵式或等值于蕴涵式的命题，如析取式、等值式。
在形式证明中可以根据需要随时使用条件证明规则。
例5 A →（B∧D）
B →（（C→（C∨E））→F） / ∴ A→F
解：① A →（B∧D） P
② B →（（C→（C∨E））→F）P
③ A
④ B∧D ①③MP
⑤ B ④∧-
⑥（C→（C∨E））→F ②⑤MP
⑦ C
⑧ C∨E ⑦∨+
⑨ C →（C∨E） ⑥-⑦C?P
⑩ F ⑥⑨MP
⑾ A→F ③-⑩C?P
2．5 间接证明规则RAA
间接证明又叫做归谬证明或反证法。这是一种在数学中经常用到的证明方法。当我们要证明某一定理时，先引入该定理的否定为假设。然后由这一假设推导出矛盾。由于矛盾是不可能的，假设一定错误，即该定理的否定不成立。由此就间接地证明了该定理成立。
间接证明规则就是根据这一思路得到的。当我们为一有效推理建立形式证明时，不是直接去证明由前提推演出结论，而是将结论的否定作为一个补充前提引入形式证明。然后由扩充的前提集合推演出一个矛盾：即演出一个形式为“p∧?p”的命题公式。由这个矛盾我们实际上推演出对这个补充前提的否定，即对结论的否定的否定，再根据双否律DN，就相当于推演出结论。
例6 A→（B∧C）
（B∨D）→E
D∨A / ∴E
解 ⑴ A→（B∧C） P
⑵（B∨D）→E P
⑶ D∨A P / ∴ E
⑷ ?E RAA
⑸ ?（B∨D） ⑵⑷ MT
⑹ ?B∧?D ⑸DeM
⑺ ?D ⑹ COM，∧-
⑻ A ⑶⑺ ∨-
⑼ B∧C ⑴⑻ MP
⑽ B ⑼ ∧-
⑾ ?B ⑹ ∧-
⑿ B∧?B ⑽⑾ ∧+
在这个形式证明中，公式⑷是结论“E”的否定，它是作为补充前提引入证明的。证明的最后一步是公式⑿，它是一个矛盾式，恒为假。如果推理是有效的，前提真时结论必真。现在由于引入补充前提⑷而推出了假结论，因此公式⑷这个补充前提一定不成立。⑷不成立即结论的否定不成立，即“ E”，根据双否律推出“E”。“E”即结论，因此结论成立。
由例6可见，运用间接证明规则就是将结论的否定作为补充前提引入证明，最后推出矛盾。由此间接地证明结论成立，推理有效。
2．6 证明重言式
我们前面讨论的形式证明是关于有效推理的证明。在一个有效的推理中，结论是依赖于前提的，前提真时结论必真。因此结论的真是有条件的。
然而有一种命题的真是无条件的，不依赖于其它命题。这样的命题就是重言式。形式证明同样适用于证明重言式。可以证明重言式是不需要任何前提就可以推演出的命题。
虽然证明重言式不需要任何前提，但建立形式证明需要有出发点。这意味着我们只能用条件证明或者间接证明的方法来证明重言式，因为只有这两种方法可以引入假设前提。我们以假设前提为出发点就能建立重言式的形式证明。
用条件证明方法证明重言式就是先引入假设前提，然后逐步消去所有假设前提而推演出一个公式，这个命题公式就是不依赖于任何前提的重言式。
例7 证明A→（B→A）是重言式。
证： ① A
② A∨?B ①∨+
③ ?B∨A ② Com
④ B→A ③ Impl
⑤ A→(B→A) ①-④ C?P
再举一例：
例8 证明（（p→q）∧p）→q是个重言式。
证： ①（p→q）∧p
② p→q ①∧-
③ p ① Com, ∧-
④ q ②③ MP
⑤ （（p→q）∧p）→q ①-④ C?P
例8中的重言式“（（p→q）∧p）→q”是一个与分离规则MP等价的蕴涵式。实际上，任意一个有效推理都等价于一个重言的蕴涵式。因为在建立该推理的形式证明时，我们可以反复运用条件证明规则，消去每个前提而使其成为结论的构成部分。由此我们将得到一个蕴涵式，而有关推理有效性的形式证明同时也证明了这个蕴涵式是重言式。
用间接证明方法证明重言式则是将所证公式的否定引入作为假设前提，然后推出矛盾。否定一个公式将导致逻辑矛盾，那么这个公式一定是重言式。
例9 证明A→（A∨B）是重言式。
证： ① ?（A→（A∨B））
② ?（?A∨（A∨B）） ① Impl
③ A ∧ ?（A∨B） ② DeM
④ A ∧（?A∧?B） ③ DeM
⑤（A∧?A）∧?B ④ Ass
⑦ A∧?A ⑤ ∧-
显然，作为重言式的命题不同于必须给定前提才能推演出的命题，后者的真是有条件的，重言式的真则是无条件的。正因为这样，一个命题公式是重言式，那么我们不需要任何其它公式为前提就可以把这个公式推演出来。因此，如果说形式证明是证明一个推理的有效性，那么关于重言式的形式证明就相当于证明一个只有结论而没有前提的推理的有效性。
