演绎定理

维基百科，自由的百科全书

在数理逻辑中，演绎定理声称如果公式 F 演绎自 E，则蕴涵 E → F 是可证明的(就是或它可以自空集推导出来)。用符号表示，如果 $E \vdash F$ ，则 $\vdash E \rightarrow F$ 。

演绎定理可以推广到假定公式的可数序列，使得从

$E_1, E_2, ... , E_{n-1}, E_n \vdash F$ ，推出 $E_1, E_2, ... , E_{n-1} \vdash E_n \rightarrow F$ ，等等直到 $\vdash E_1\rightarrow(...(E_{n-1} \rightarrow (E_n \rightarrow F))...)$ 。

演绎定理是元定理: 在给定的理论中使用它来演绎证明，但它不是这个理论自身的一个定理。

演绎元定理是最重要的元定理之一。在某些逻辑系统中，它被接受为是 "→" 的介入规则的一个推理规则。在其他系统中，从公理证明它是证明这个逻辑是完备的首要任务。不使用演绎元定理在命题逻辑中证明任何东西都是非常困难的。如果你使用了它通常就很容易了。

[编辑] 自然演绎的例子

"证明"公理 1: P→(Q→P)

- P 1. 假设
  - Q 2. 架设
  - P 3. 重复 1
- Q→P 4. 演绎自 2 到 3
P→(Q→P) 5. 演绎自 1 到 4 QED

"证明"公理 2: (P→(Q→R))→((P→Q)→(P→R))

- P→(Q→R) 1. 假设
  - P→Q 2. 假设
    - P 3. 假设
    - Q 4. 肯定前件 3,2
    - Q→R 5. 肯定前件 3,1
    - R 6. 肯定前件 4,5
  - P→R 7. 演绎自 3 到 6
- (P→Q)→(P→R) 8. 演绎自 2 到 7
(P→(Q→R))→((P→Q)→(P→R)) 9. 演绎自 1 到 8 QED

使用公理 1 证明 ((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

[编辑] 虚拟的推理规则

从例子中，我们可以见到已经我们的正常公理化逻辑增加了三个虚拟(或额外和临时)的推理规则。它们是"假设"、"重复"和"演绎"。正规的推理规则(比如"肯定前件"和各种公理)仍是可用的。

1. 假设向那些已经获得的前提增加一个额外的前提的步骤。所以，如果你的前面步骤 S 演绎为:

$E_1, E_2, ... , E_{n-1}, E_n \vdash S$ ，

则你增加另一个前提 H 并得到:

$E_1, E_2, ... , E_{n-1}, E_n, H \vdash H$ 。

这符号化了从第 n 层缩进移进到第 n+1 层：

S 前面的步骤
- H 假设

2. 重复是重新使用前面的步骤的一个步骤。在实践中，这只在你希望采用一个不是最近假设的假设，并把它用为在演绎步骤之前的最终步骤的时候才是需要的。

3. 演绎是你去除最近假设(仍可用)并把它前缀于前面步骤的步骤。这被展示为下面这样的去缩进一层:

- H 假设
- ......... (其他步骤)
- C (结论自 H)
H→C 演绎

[编辑] 从使用演绎元定理的演绎转换到公理化证明

在公理化版本的命题逻辑中，通常有着公理模式和推理规则(这里的 P、Q 和 R 可以被替换为任何命题)：

公理 1：P→(Q→P)
公理 2：(P→(Q→R))→((P→Q)→(P→R))
推理规则肯定前件：从 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 之前并且因此也在这个范围之外。

[编辑] 转换的例子

要展示如何把自然演绎转换成公理化形式的证明，我们应用它于重言式 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

[编辑] 逆定理

这个定理的逆命题也成立。它从是蕴涵除去规则的肯定前件立即得出。

[编辑] 参见

[编辑] 引用

Introduction to Mathematical Logic by Vilnis Detlovs and Karlis Podnieks Podnieks is a comprehensive tutorial. See Section 1.5.

来自“http://zh.wikipedia.org../../../%E6%BC%94/%E7%BB%8E/%E5%AE%9A/%E6%BC%94%E7%BB%8E%E5%AE%9A%E7%90%86.html”

页面分类: 數理邏輯 | 定理

We provide Linux to the World