上一页

ⓘ 演绎定理




演绎定理
                                     

ⓘ 演绎定理

在数理逻辑中, 演绎定理 声称如果公式 F 演绎自 E,则蕴涵 E → F 是可证明的。用符号表示,如果 E ⊢ F {\displaystyle E\vdash F} ,则 ⊢ E → F {\displaystyle \vdash E\rightarrow F} 。

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

E 1, E 2., E n − 1, E n ⊢ F {\displaystyle E_{1},E_{2}.,E_{n-1},E_{n}\vdash F} ,推出 E 1, E 2., E n − 1 ⊢ E n → F {\displaystyle E_{1},E_{2}.,E_{n-1}\vdash E_{n}\rightarrow F} ,等等直到 ⊢ E 1 →. E n − 1 → E n → F) {\displaystyle \vdash E_{1}\rightarrow.E_{n-1}\rightarrow E_{n}\rightarrow F)} 。

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

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

                                     

1. 演绎的例子

证明”公理 1: P→Q→P

  • P 3. 重复 1
  • Q 2. 假设
  • P 1. 假设
  • Q→P 4. 演绎自 2 到 3
  • P→Q→P 5. 演绎自 1 到 4 QED

证明”公理 2: P→Q→R)→P→Q→P→R)

  • Q→R 5. 肯定前件 3.1
  • P→Q→R 1. 假设
  • P 3. 假设
  • Q 4. 肯定前件 3.2
  • P→Q 2. 假设
  • 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 2. 公理 1
  • P→Q→P)→R 1. 假设
  • R 3. 肯定前件 2.1
  • P→Q→P)→R)→R 4. 演绎自 1 到 3 QED
                                     

2. 虚拟的推理规则

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

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

E 1, E 2., E n − 1, E n ⊢ S {\displaystyle E_{1},E_{2}.,E_{n-1},E_{n}\vdash S} ,

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

E 1, E 2., E n − 1, E n, H ⊢ H {\displaystyle E_{1},E_{2}.,E_{n-1},E_{n},H\vdash H} 。

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

  • S 前面的步骤
  • H 假设

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

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

  • . 其他步骤
  • H 假设
  • C 结论自 H
  • H→C 演绎
                                     

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

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

  • 公理 1:P→H→P
  • 推理规则肯定前件:从 P 和 P→Q 推出 Q
  • 公理 2:H→P→Q)→H→P→H→Q)

从这些公理和推理规则你可以快速的演绎出定理模式 P→P 参见命题演算。选择这些公理模式使你能够容易的从它们推导出演绎定理。可以通过使用真值表验证来证实它们为重言式,而肯定前件保持真理。

假如我们有了 Γ 与 H 证明 C,并且我们希望证实 Γ 证明 H→C。对于在演绎中的每个步骤 S:

  • 如果这个步骤是应用肯定前件于 A 和 A→S 的结果,我们首先确保它们已经被转换成 H→A 和 H→A→S,并接着采用公理 2:H→A→S)→H→A→H→S),并应用肯定前件来得到 H→A→H→S,并接着再次应用来得到 H→S。
  • 如果这个步骤是在 Γ 中的前提重复步骤或一个公理,我们可以应用肯定前件于公理 1:S→H→S,来得到 H→S。
  • 如果这个步骤是 H 自身假设步骤,我们应用这个定理模式来得到 H→H。

在这个证明的结束处我们有了所需要的 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 演算项到组合子逻辑项的转换过程,这里的公理 1 对应于 K 组合子,而公理 2 对应于 S 组合子。注意 I 组合子对应于定理模式 P→P。



                                     

4. 转换的例子

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

首先,我们写使用自然演绎的证明:

  • Q→R 2. 假设
  • R 3. 肯定前件 1.2
  • Q 1. 假设
  • Q→R→R 4. 演绎自 2 到 3
  • Q→Q→R→R) 5. 演绎自 1 到 4 QED

其次,我们转换内层的演绎为公理化证明:

  • Q 5. 假设
  • Q→R→Q→R 1. 定理模式 A→A
  • Q→Q→R→Q) 4. 公理 1
  • Q→R→Q→R)→Q→R→Q)→Q→R→R) 2. 公理 2
  • Q→R→Q)→Q→R→R) 3. 肯定前件 1.2
  • Q→R→R 7. 肯定前件 6.3
  • Q→R→Q 6. 肯定前件 5.4
  • Q→Q→R→R) 8. 演绎自 5 到 7 QED

第三,我们转换外层的演绎为公理化证明:

  • Q→R→Q)→Q→R→R) 3. 肯定前件 1.2
  • Q→R→Q→R)→Q→R→Q)→Q→R→R) 2. 公理 2
  • Q→R→Q→R 1. 定理模式 A→A
  • Q→Q→R→R) 9. 肯定前件 4.8 QED
  • Q→Q→R→Q) 4. 公理 1
  • 8. 肯定前件 6.7

这三个步骤可以简洁的使用Curry-Howard同构表述为:

  • 其次,通过在 b 上的 lambda 除去,f = λa. s i k a
  • 首先,在 lambda 演算中,函数 f = λa. λb. b a 有类型 q → q → r → r
  • 第三,通过在 a 上的 lambda 除去,f = s k s i) k
                                     

5. 逆定理

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

                                     

6. 参见

  • 自然演绎
  • 皮尔士定律
  • 蕴涵命题演算
  • 相继式演算
  • 演绎推理
  • 希尔伯特演绎系统