查看“︁演绎定理”︁的源代码

'''演绎定理'''是[[数理逻辑]]的一個核心規則，它清晰地描述[[元語言]]的純符號組合所做的演繹與[[逻辑语言]]裡的[[实质条件]]的聯繫。

== 簡介 ==
演绎定理通常被視為[[元定理]]，也就是以元語言來描述的符號組合規則（也就是[[推理规则]]，如[[肯定前件]]）為基礎，配上邏輯公理（被認為＂永遠為真＂的一套[[合式公式]]）為前提去證明的某種規則，通常都有以下的形式：（以下<math>\mathcal{A}_1,\,\cdots,\,\mathcal{A}_n</math> 、 <math>\mathcal{B}</math> 為任意[[合式公式]]）

:「若根據前提 <math>\mathcal{A}_1,\,\cdots,\,\mathcal{A}_n</math> 和[[公理]]與[[推理规则]]，可以推出 <math>\mathcal{B}</math> ，那對任意 <math>1\leq\mathcal{i}\leq n</math> 也可以推出 <math>\mathcal{A_i}\Rightarrow\mathcal{B}</math>」

視為元定理的例子請參見[[一阶逻辑#演繹元定理|一阶逻辑條目的演繹元定理]]。

但在某些[[逻辑]]系统中，演绎定理被定為基礎的[[推理规则]]。這種系統跟視為元定理的系統比較起來，推理的效力是等同的，所以在此並不贅述。

==演绎的例子==
证明 ((P→(Q→P))→R)→R:
**(P→(Q→P))→R 1. 假设
**P→(Q→P) 2. 公理 1
**R 3. 肯定前件 2,1
*((P→(Q→P))→R)→R 4. 演绎自 1 到 3 QED

==从使用演绎元定理的演绎转换到公理化证明==

在公理化版本的命题逻辑中，通常有着公理模式和推理规则(这里的 P、Q 和 H 可以被替换为任何命题)：
*公理 1：P→(H→P)
*公理 2：(H→(P→Q))→((H→P)→(H→Q))
*推理规则[[肯定前件]]：从 P 和 P→Q 推出 Q
从这些公理和推理规则你可以快速的演绎出定理模式 P→P (参见[[命题演算]])。选择这些公理模式使你能够容易的从它们推导出演绎定理。可以通过使用真值表验证来证实它们为重言式，而肯定前件保持真理。

假如我们有了 Γ 与 H 证明 C，并且我们希望证实 Γ 证明 H→C。对于在演绎中的每个步骤 S:
* 如果这个步骤是在 Γ 中的前提(重复步骤)或一个公理，我们可以应用肯定前件于公理 1：S→(H→S)，来得到 H→S。
* 如果这个步骤是 H 自身(假设步骤)，我们应用这个定理模式来得到 H→H。
* 如果这个步骤是应用肯定前件于 A 和 A→S 的结果，我们首先确保它们已经被转换成 H→A 和 H→(A→S)，并接着采用公理 2：(H→(A→S))→((H→A)→(H→S))，并应用肯定前件来得到 (H→A)→(H→S)，并接着再次应用来得到 H→S。
在这个证明的结束处我们有了所需要的 H→C，除了它现在只依赖于 Γ 而不再依赖于 H 之外。所以这个演绎步骤将消失，合并到是从 H 推导出的结论的前面步骤中。

为了最小化结果证明的复杂性，在转换之前要进行某些预处理。实际上不依赖于 H 的任何步骤(除了结论)都应当被移动到假设步骤之前并去缩进一个层次。并且任何其他不必要步骤(不用来得到结论或可以被绕过的)，比如不是结论的重复应当除去。

在转换期间，在演绎开始处(紧接着 H→H 步骤之后)放置所有的对公理 1 的肯定前件应用可能是有用的。

在转换肯定前件的时候，如果 A 在 H 的范围之外，则必须应用公理 1：A→(H→A)，和肯定前件来得到 H→A。类似的，如果 A→S 在 H 的范围之外，应用公理 1：(A→S)→(H→(A→S)) 和肯定前件来得到 H→(A→S)。做这二者不是必须的，除非肯定前件步骤是结论，因为二者都在这个范围之外，那么肯定前件应当已经被移动到 H 之前并且因此也在这个范围之外。

在[[Curry-Howard同构]]下，上述对演绎元定理的转换过程类似于从[[lambda 演算]]项到[[组合子逻辑]]项的[[组合子逻辑#S-K 基的完备性|转换过程]]，这里的公理 1 对应于 K 组合子，而公理 2 对应于 S 组合子。注意 I 组合子对应于定理模式 P→P。

==转换的例子==
要展示如何把[[自然演绎]]转换成公理化形式的证明，我们应用它于重言式 Q→((Q→R)→R)。实际上，知道可以这么做通常就足够了。我们通常使用自然演绎形式来替代更长的公理化证明。

首先，我们写使用自然演绎的证明:
**Q 1. 假设
***Q→R 2. 假设
***R 3. 肯定前件 1,2
**(Q→R)→R 4. 演绎自 2 到 3
*Q→((Q→R)→R) 5. 演绎自 1 到 4 QED

其次，我们转换内层的演绎为公理化证明:
*(Q→R)→(Q→R) 1. 定理模式 (A→A)
*((Q→R)→(Q→R))→(((Q→R)→Q)→((Q→R)→R)) 2. 公理 2
*((Q→R)→Q)→((Q→R)→R) 3. 肯定前件 1,2
*Q→((Q→R)→Q) 4. 公理 1
**Q 5. 假设
**(Q→R)→Q 6. 肯定前件 5,4
**(Q→R)→R 7. 肯定前件 6,3
*Q→((Q→R)→R) 8. 演绎自 5 到 7 QED

第三，我们转换外层的演绎为公理化证明:
*(Q→R)→(Q→R) 1. 定理模式 (A→A)
*((Q→R)→(Q→R))→(((Q→R)→Q)→((Q→R)→R)) 2. 公理 2
*((Q→R)→Q)→((Q→R)→R) 3. 肯定前件 1,2
*Q→((Q→R)→Q) 4. 公理 1
*[((Q→R)→Q)→((Q→R)→R)]→[Q→(((Q→R)→Q)→((Q→R)→R))] 5. 公理 1
*Q→(((Q→R)→Q)→((Q→R)→R)) 6. 肯定前件 3,5
*[Q→(((Q→R)→Q)→((Q→R)→R))]→([Q→((Q→R)→Q)]→[Q→((Q→R)→R))]) 7. 公理 2
*[Q→((Q→R)→Q)]→[Q→((Q→R)→R))] 8. 肯定前件 6,7
*Q→((Q→R)→R)) 9. 肯定前件 4,8 QED

这三个步骤可以简洁的使用[[Curry-Howard同构]]表述为:
*首先，在 lambda 演算中，函数 f = λa. λb. b a 有类型 q → (q → r) → r
*其次，通过在 b 上的 lambda 除去，f = λa. s i (k a)
*第三，通过在 a 上的 lambda 除去，f = s (k (s i)) k

==参见==
*[[皮尔士定律]]
*[[演绎推理]]
*[[自然演绎]]
*[[相继式演算]]
*[[希尔伯特演绎系统]]
*[[蕴涵命题演算]]

==引用==
* [http://www.ltn.lv/~podnieks/mlog/ml.htm Introduction to Mathematical Logic by Vilnis Detlovs and Karlis Podnieks] {{Wayback|url=http://www.ltn.lv/~podnieks/mlog/ml.htm |date=20100214150910 }}  Podnieks is a comprehensive tutorial.  See Section 1.5.

==外部链接==
*[http://us.metamath.org/mpegif/mmset.html 元数学证明探索者主页] {{Wayback|url=http://us.metamath.org/mpegif/mmset.html |date=20090825231525 }}

[[Category:數理邏輯|Y]]
[[Category:数学定理|Y]]