演绎定理
简介
演绎定理通常被视为元定理,也就是以元语言来描述的符号组合规则(也就是推理规则,如肯定前件)为基础,配上逻辑公理(被认为"永远为真"的一套合式公式)为前提去证明的某种规则,通常都有以下的形式:(以下 、 为任意合式公式)
视为元定理的例子请参见一阶逻辑条目的演绎元定理。
但在某些逻辑系统中,演绎定理被定为基础的推理规则。这种系统跟视为元定理的系统比较起来,推理的效力是等同的,所以在此并不赘述。
演绎的例子
证明 ((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 演算项到组合子逻辑项的转换过程,这里的公理 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 1. 假设
- 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
参见
引用
- Introduction to Mathematical Logic by Vilnis Detlovs and Karlis Podnieks (页面存档备份,存于互联网档案馆) Podnieks is a comprehensive tutorial. See Section 1.5.
外部链接
- 元数学证明探索者主页 (页面存档备份,存于互联网档案馆)