查看“︁蕴涵命题演算”︁的源代码

在[[数理逻辑]]中，'''蕴涵命题演算'''是只使用叫做蕴涵或条件的一个[[逻辑连结词|连结词]]的经典(二值)[[命题演算]]。用[[公式 (数理逻辑)|公式]]表达，这个[[二元运算]]被指示为“implies”
“如果 ..., 则 ...”, “→”, “<math>\rightarrow \!</math>”等等。

==作为算子的实质完备性==

单独的蕴涵作为[[逻辑算子]]不是完备的，因为不能用它形成所有其他二值[[真值函数]]。但是如果有已知为假的一个[[命题]]并作为给虚假的零元连结词那样使用它，则可以定义所有其他真值函数。所以蕴涵作为算子实质上是完备的。如果 P,Q 和 F 是命题而 F 已知为假，则:
*¬P [[逻辑等价|等价]]于 P→F
*P∧Q 等价于 (P→(Q→F))→F
*P∨Q 等价于 (P→F)→Q
*P↔Q 等价于 ((P→Q)→((Q→P)→F))→F

更一般的说，因为上述算子对表达任何真值函数是[[必要和充分条件|充分]]的，可以得出任何真值函数都依据“→”和“F”来表达，如果有一个命题 F 已知为假。

==公理==

*[[公理]][[公理模式|模式]] 1 是 P→(H→P)。
*公理模式 2 是 (H→(P→Q))→((H→P)→(H→Q))。
*公理模式 3 ([[皮尔士定律]])是 ((P→Q)→P)→P。
*唯一的[[推理规则]]([[肯定前件]])是: 从 P 和 P→Q 推出 Q。
在这里每个情况下，P, Q, H 可以被替代为只包含“→”作为连结词的任何命题。

==演绎元定理==

首要任务是使用公理 1, 2 和肯定前件导出[[演绎推理|演绎]]元定理。

我们开始于证明一个定理模式(这里的 A 和 B 可替代为只包含“→”作为连结词的任何命题):
*(A→((B→A)→A))→((A→(B→A))→(A→A)) 1. 公理 2
*A→((B→A)→A) 2. 公理 1
*(A→(B→A))→(A→A) 3. 肯定前件 2,1
*A→(B→A) 4. 公理 1 
*A→A 5. 肯定前件 4,3 [[Q.E.D. |QED]]

后续过程详见[[演绎定理]]。

==取代虚假==

如果 A 和 Z 是命题，则 A→Z 等价于 (¬A*)∨Z，这里的 A* 是把 A 中 Z 的所有、某个或零个出现替代为虚假的结果。类似的，(A→Z)→Z 等价于 A*∨Z。所以在某些条件下，它们可以分别作为表说 A* 为假或 A* 为真的替代品。

==公理的完备性，第一部分==

我们将看到这些公理在任何只包含“→”作为连结词的[[重言式]]都可用从它们演绎出的意义上。考虑只包含 P1, P2, ..., Pn 作为原子命题(命题变量)的重言式 S。

在真值表中选择一行给 S。它展示了对一个特定賦值(从命题变量到 {假, 真} 的函数)每个 S 的子公式的真值。通过在子公式长度上的[[数学归纳法]]，我们将证实从形如 Pk→Z (在 Pk 被给予值假的时候)或(Pk→Z)→Z (在 Pk 被给予值真的时候)的命题，可以为每个 S 的子公式演绎出类似的命题。这需要下面给出的三个[[引理]]。

===真结论的引理===

考虑 S 的子公式 P→Q。如果 Q 被賦值给予值[[真理|真]]，则 P→Q 也将被给予值真。所以我们需要证实 ((P→Q)→Z)→Z 可以证明自关于这个賦值的[[假定]]。

**(Q→Z)→Z 1. [[假设]]
***(P→Q)→Z 2. 假设
****Q 3. 假设
*****P 4. 假设
*****Q 5. 重复 3
****P→Q 6. 演绎自 4 到 5
****Z 7. 肯定前件 6,2
***Q→Z 8. 演绎自 3 到 7
***Z 9. 肯定前件 8,1
**((P→Q)→Z)→Z 10. 演绎自 2 到 9
*((Q→Z)→Z)→(((P→Q)→Z)→Z) 11. 演绎自 1 到 10 QED

===假前提的引理===

如果 P 被賦值给予值假，则 P→Q 将给给予值真。所以我们需要证实 ((P→Q)→Z)→Z 可以证明自关于这个賦值的假定。

**P→Z 1. 假设
***(P→Q)→Z 2. 假设
****Z→Q 3. 假设
*****P 4. 假设
*****Z 5. 肯定前件使用步骤 4 和 1
*****Q 6. 肯定前件使用步骤 5 和 3
****P→Q 7. 演绎自 4 到 6
****Z 8. 肯定前件使用步骤 7 和 2
***(Z→Q)→Z 9. 演绎自 3 到 8
***((Z→Q)→Z)→Z 10. 皮尔士定律
***Z 11. 肯定前件使用步骤 9 和 10
**((P→Q)→Z)→Z 12. 演绎自 2 到 11
*(P→Z)→((P→Q)→Z)→Z) 13. 演绎自 1 到 12 QED

===真前提和假结论的引理===

如果 P 被賦值给予值真而 Q 被给予值假，则 P→Q 将被给予值假。所以我们需要证明 (P→Q)→Z 可以证明自关于这个賦值的假定。

**(P→Z)→Z 1. 假设
***Q→Z 2. 假设
****P→Q 3. 假设
*****P 4. 假设
*****Q 5. 肯定前件 4,3
*****Z 6. 肯定前件 5,2
****P→Z 7. 演绎自 4 到 6
****Z 8. 肯定前件 7,1
***(P→Q)→Z 9. 演绎自 3 到 8
**(Q→Z)→((P→Q)→Z) 10. 演绎自 2 到 9
*((P→Z)→Z)→[(Q→Z)→((P→Q)→Z)] 11. 演绎自 1 到 10 QED

==公理的完备性，第二部分==

在完备性证明的第一部分，我们证实了假定关于命题变量的适当假设，(S→Z)→Z 可以证明自重言式 S 每个賦值。现在我们将把这些賦值合并起来并除去关于命题变量的假定。

考虑仍未从假定中除去的命题变量中的一个，比如它是 P。则使用演绎元定理，我们得到 (P→Z)→((S→Z)→Z) 并且类似的我们得到 ((P→Z)→Z)→((S→Z)→Z)，二者都从 P 不出现的假定的简约集合中得出。

**(P→Z)→((S→Z)→Z) 1. 假设
***((P→Z)→Z)→((S→Z)→Z) 2. 假设
****S→Z 3. 假设
*****P→Z 4. 假设
*****(S→Z)→Z 5. 肯定前件 4,1
*****Z 6. 肯定前件 3,5
****(P→Z)→Z 7. 演绎自 4 到 6
****(S→Z)→Z 8. 肯定前件 7,2
****Z 9. 肯定前件 3,8
***(S→Z)→Z 10. 演绎自 3 到 9
**[((P→Z)→Z)→((S→Z)→Z)]→[(S→Z)→Z] 11. 演绎自 2 到 10
*[(P→Z)→((S→Z)→Z)]→([((P→Z)→Z)→((S→Z)→Z)]→[(S→Z)→Z]) 12. 演绎自 1 到 11 QED

所以我们可以组合成对的真值表的行到一起并重复这个过程直到关于命题变量的值的假定都被除去了。结果将是我们已经证明了 (S→Z)→Z，这里的 S 是重言式而 Z 是任何命题。现在我们选择 Z 一样于 S。因此 (S→S)→S 是个定理只要 S 是重言式。但是 S→S 是我们早先证明的定理模式的一个实例。所以通过肯定前件 S 是对于任何重言式 S 的一个定理。我们的公理是完备的。

这个证明是构造性的。就是说给定一个重言式，我们可以服从指导并从我们的公理建立它的一个证明。但是，这种证明的长度随着重言式中命题变量的数目呈超指数增长。所以除了对非常短的重言式之外它不是实用性的方法。

==在完备性定理中的排中律==

有趣的是排中律(皮尔士定理形式的公理 3)只在我们的完备性证明中出现了一次。

相反的，Mendelson 命题逻辑的完备性证明在很多地方使用了排中律，特别是在把真值表的行合并在一起来除去命题变量依赖的步骤中。他使用了他的第三个公理 (¬A→¬B)→((¬A→B)→A) 来推导 (A→B)→((¬A→B)→B)，它接着被用来合并真值表的行到一起。

==参见==
*[[命题演算]]
*[[演绎定理]]
*[[皮尔士定律]]
*[[重言式]]
*[[真值表]]
*[[賦值 (邏輯)|賦值]]

==引用==
* Mendelson, Elliot (1997) [http://worldcat.org/oclc/259359 Introduction to Mathematical Logic, 4th ed.] {{Wayback|url=http://worldcat.org/oclc/259359 |date=20070929141903 }} London: Chapman & Hall.

[[Category:逻辑演算]]