Suppes–Lemmon 式自然演绎
| Suppes–Lemmon 式自然演绎 | |
|---|---|
| 术语名称 | Suppes–Lemmon 式自然演绎 |
| 英语名称 | Suppes–Lemmon natural deduction |
| 别名 | Suppes–Lemmon notation |
Suppes–Lemmon 式自然演绎(Suppes–Lemmon natural deduction)是逻辑领域形式化公理系统中 Gentzen 式系统中自然演绎系统的一种。其中每行都是一个公式，这些公式会标注出其使用的规则以及依赖的公式，以反映公式间的变形关系。 Suppes–Lemmon 式自然演绎是 Fitch 式自然演绎的一个修改版，其的特征是画成表格形态，各行之间书写成一个并列、有行号的列表，各行之间的直接依赖关系通过注明依赖行号表达，而间接依赖的全部假设通过表格中专门的一列表达； Suppes–Lemmon 式自然演绎中不再使用假设开启子证明，而是直接引入假设行表达假言推理，在 Fitch 式自然演绎系统中用于表达当前证明中有效假设的子证明被依赖假设取代。
说明：有部分材料使用的记号与现代标准记号不同，以下均按照现代记号表示。
描述
以下是 [math]\displaystyle{ p\rightarrow q\rightarrow p }[/math] 的一个证明。
| [math]\displaystyle{ \vdash p\rightarrow q\rightarrow p }[/math] | |||
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| 1 | [math]\displaystyle{ p }[/math] | A (CP) | 1 |
| 2 | [math]\displaystyle{ q }[/math] | A (CP) | 2 |
| 3 | [math]\displaystyle{ p }[/math] | 1 R | 1,2 |
| 4 | [math]\displaystyle{ q\rightarrow p }[/math] | 2,3 CP | 1 |
| 5 | [math]\displaystyle{ p\rightarrow q\rightarrow p }[/math] | 1,4 CP | |
| Q.E.D. | |||
以下是从 [math]\displaystyle{ p\rightarrow q }[/math] 到 [math]\displaystyle{ \lnot q \rightarrow \lnot p }[/math] 的一个演绎：
| [math]\displaystyle{ p\rightarrow q \vdash \lnot q \rightarrow \lnot p }[/math] | |||
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| 1 | [math]\displaystyle{ p\rightarrow q }[/math] | A | 1 |
| 2 | [math]\displaystyle{ ¬q }[/math] | A (CP) | 2 |
| 3 | [math]\displaystyle{ p }[/math] | A (RAA) | 3 |
| 4 | [math]\displaystyle{ q }[/math] | 1,3 MP | 1,3 |
| 5 | [math]\displaystyle{ q\land ¬q }[/math] | 2,4 ∧I | 1,2,3 |
| 6 | [math]\displaystyle{ \lnot p }[/math] | 3,5 RAA | 1,2 |
| 7 | [math]\displaystyle{ \lnot q\rightarrow\lnot p }[/math] | 2,6 CP | 1 |
| Q.E.D. | |||
符号及术语说明
- 部分材料中，记号可能有微小差异，请以具体记号为准。
- 演绎过程中的每一个公式称为一行(line)，且表格中的一行包括行号、公式、变形规则、依赖假设四列。
- 每行右侧有这一行使用的变形规则及其依赖行号，或仅指出这是一个假设而非变形结果。
- 最后一行是 Q.E.D. ，代表证明结束，上一行是结论(conclusion)。也有的材料中不写这一行。证明中的结论为要证公式本身，演绎中的结论为仅以前提为假设的要证公式。
特征
- 每行都是形式语言中的一个公式。
- 每个行或者是假设，或者依赖一个或多个其他行。
- 证明中的每行都在这一行所依赖的前提下为真。其中所依赖的前提指这行右侧给出的依赖行号。如上例中第 5 行的 [math]\displaystyle{ q\land \lnot q }[/math] 的依赖为 1,2,3 ，因此所依赖的前提是第 1 行、第 2 行和第 3 行，即 [math]\displaystyle{ q\land\lnot q }[/math] 在条件 [math]\displaystyle{ p\rightarrow q, \lnot q, p }[/math] 下成立（尽管本身是矛盾式，这里是因为前提也有矛盾，矛盾能推出任意公式）。
记号约定
公式描述
Suppes–Lemmon 式自然演绎中使用的形式语言和命题语言、谓词语言的定义相同。
命题描述
一个证明或一个需证明命题通常被写成后继式 [math]\displaystyle{ \Gamma, \Delta, \phi \vdash \psi }[/math] 的形式，其中左侧可以包括前提集合 [math]\displaystyle{ \Gamma,\Delta }[/math] ，也可以包括单个前提 [math]\displaystyle{ \phi }[/math] ，不止一个则通过逗号隔开，右侧是单个结论 [math]\displaystyle{ \psi }[/math] 。
变形规则描述
一个变形规则总是写成形式 [math]\displaystyle{ H_1\quad\cdots\quad H_n\vdash C }[/math] 。其中左侧是前提，可以包括一个至多个公式 [math]\displaystyle{ H_1,\cdots,H_n }[/math] ，若不止一个则多个前提间需用逗号隔开，且多个前提间不要求顺序（部分材料中可能要求顺序与在规则列标注顺序一致）。右侧是结论，只能有一个公式 [math]\displaystyle{ C }[/math] 。每个变形规则中，新结论 [math]\displaystyle{ C }[/math] 依赖项的计算规则也会被强制指定。
每个变形规则都有一个名称。基础规则由逻辑联结词的引入、消除规则构成，用逻辑联结词和 I （引入(introduction)）或 E （消去(elimination)）命名。非基础规则也使用定理名称或缩写。但是不同材料中记号可能有区别，如 [math]\displaystyle{ \land_I }[/math] 可能被记作 [math]\displaystyle{ \land_\mathrm{I} }[/math] 、 [math]\displaystyle{ \land I }[/math] 、 [math]\displaystyle{ \land\mathrm{I} }[/math] ，其他记号也依此类推。可以存在非基础的变形规则，但由于变形规则总是能归结于符号的变化，理论上合理的变换规则总是能拆分成基础规则。此外，通过切消定理，对于常见的证明过程可以作为新规则引入。
变形规则结论依赖项一般是其前提依赖项的并集，并从中去除构成这个规则的假设。
基本变形规则
Suppes–Lemmon 式自然演绎中有几个通用的操作：
- 进行一个公式假设，如果不是前提，在被消除时需要标注这一假设的目的是使用何种变形规则。规则列记为“ A (S) ”，其中 S 替换为具体变形规则名称。
- 应用某种规则，从几个行前提得到新的公式。此时规则列标注所涉及的行数以及规则名称。
- 重复：可以重复之前的任意一行，保持其原有依赖假设不变，也可以为其增加新的假设。规则列记为“ a R ”。
需要注意两点：
- 对下述规则，这些前提行出现顺序是固定的，规则列中的行号总是从小到大排列。
- 部分材料中可能不存在重复规则，无法调整前提行顺序，此时规则中前提行的顺序不再限制。规则列前提行的行号需要按照实际内容符合情况对应，可能不再是从小到大的排列。
命题逻辑
关于命题逻辑的 Suppes–Lemmon 式自然演绎系统，可能包括以下规则。其中 [math]\displaystyle{ \phi,\psi,\chi }[/math] 可以代入为任意公式。
- 否定引入（[math]\displaystyle{ \lnot_I }[/math] 或 [math]\displaystyle{ \lnot }[/math]-int）：推出了一个假设列包含假设 [math]\displaystyle{ \phi }[/math] （行号为 a ）的矛盾（即形如 [math]\displaystyle{ \psi\land\lnot\psi }[/math] 的公式）（行号为 b ），可推出 [math]\displaystyle{ \lnot\phi }[/math] ，其依赖假设为两行假设的并集去掉 a 。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ \phi }[/math] | A (RAA) | a |
| ⋮ | ⋮ | ⋮ | ⋮ |
| b | [math]\displaystyle{ \psi\land\lnot\psi }[/math] | … | c,d,a,e,f |
| g | [math]\displaystyle{ \lnot\phi }[/math] | a,b RAA或¬I | c,d,e,f |
- 否定消去（[math]\displaystyle{ \lnot_E }[/math] 或 [math]\displaystyle{ \lnot }[/math]-elim）或双重否定消去（[math]\displaystyle{ \lnot\lnot_E }[/math] 或 [math]\displaystyle{ \lnot\lnot }[/math]-elim）：从 [math]\displaystyle{ \lnot\lnot \phi }[/math] 可推出 [math]\displaystyle{ \phi }[/math] ，其依赖假设不变。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ \lnot\lnot\phi }[/math] | … | c,d,e,f |
| b | [math]\displaystyle{ \phi }[/math] | a DN或¬¬E | c,d,e,f |
- 合取引入（[math]\displaystyle{ \land_I }[/math] 或 [math]\displaystyle{ \land }[/math]-int）：从 [math]\displaystyle{ \phi }[/math] 和 [math]\displaystyle{ \psi }[/math] 可推出 [math]\displaystyle{ \phi\land\psi }[/math] ，其依赖假设为两行假设的并集。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ \phi }[/math] | … | c,d,e,f |
| ⋮ | ⋮ | ⋮ | ⋮ |
| b | [math]\displaystyle{ \psi }[/math] | … | g,h,i,j |
| k | [math]\displaystyle{ \phi\land\psi }[/math] | a,b ∧I | c,d,e,f,g,h,i,j |
- 合取消去（[math]\displaystyle{ \land_E }[/math] 或 [math]\displaystyle{ \land }[/math]-elim）：从 [math]\displaystyle{ \phi\land\psi }[/math] 可推出 [math]\displaystyle{ \phi }[/math] 、从 [math]\displaystyle{ \phi\land\psi }[/math] 可推出 [math]\displaystyle{ \psi }[/math] ，其依赖假设不变。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ \phi\land\psi }[/math] | … | c,d,e,f |
| b | [math]\displaystyle{ \phi }[/math] | a ∧E | c,d,e,f |
- 析取引入（[math]\displaystyle{ \lor_I }[/math] 或 [math]\displaystyle{ \lor }[/math]-int）：从 [math]\displaystyle{ \phi }[/math] 可推出 [math]\displaystyle{ \phi\lor\psi }[/math] 、从 [math]\displaystyle{ \phi }[/math] 可推出 [math]\displaystyle{ \psi\lor\phi }[/math] ，其依赖假设不变。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ \phi }[/math] | … | c,d,e,f |
| b | [math]\displaystyle{ \phi\lor\psi }[/math] | a ∨I | c,d,e,f |
- 析取消去（[math]\displaystyle{ \lor_E }[/math] 或 [math]\displaystyle{ \lor }[/math]-elim）：从 [math]\displaystyle{ \phi\lor\psi }[/math] (a) 以及，依赖假设 [math]\displaystyle{ \phi }[/math] (b) 的 [math]\displaystyle{ \chi }[/math] (c) 、依赖假设 [math]\displaystyle{ \psi }[/math] (d) 的 [math]\displaystyle{ \chi }[/math] (e) ，可推出 [math]\displaystyle{ \chi }[/math] ，其依赖假设为 a,c,e 三行假设的并集中去掉 b 和 d 。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ \phi\lor\psi }[/math] | … | f,g,h,i |
| b | [math]\displaystyle{ \phi }[/math] | A (∨E) | b |
| ⋮ | ⋮ | ⋮ | ⋮ |
| c | [math]\displaystyle{ \chi }[/math] | … | b,f,g,j,k |
| d | [math]\displaystyle{ \psi }[/math] | A (∨E) | d |
| ⋮ | ⋮ | ⋮ | ⋮ |
| e | [math]\displaystyle{ \chi }[/math] | … | d,f,g,l,m |
| p | [math]\displaystyle{ \chi }[/math] | a,b,c,d,e ∨E | f,g,h,i,j,k,l,m |
- 条件引入（[math]\displaystyle{ \rightarrow_E }[/math] 或 [math]\displaystyle{ \rightarrow }[/math]-int）：从依赖假设 [math]\displaystyle{ \phi }[/math] (a) 的 [math]\displaystyle{ \psi }[/math] (b) ，可得到 [math]\displaystyle{ \phi\rightarrow\psi }[/math] ，其依赖假设为 b 的依赖中去除 a 。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ \phi }[/math] | A (CP) | a |
| ⋮ | ⋮ | ⋮ | ⋮ |
| b | [math]\displaystyle{ \psi }[/math] | … | a,g,h |
| c | [math]\displaystyle{ \phi\rightarrow\psi }[/math] | a,b CP或→I | g,h |
- 条件消去（[math]\displaystyle{ \rightarrow_E }[/math] 或 [math]\displaystyle{ \rightarrow }[/math]-elim）：从 [math]\displaystyle{ \phi\rightarrow\psi }[/math] 和 [math]\displaystyle{ \phi }[/math] 可推出 [math]\displaystyle{ \psi }[/math] ，其依赖假设为两者并集。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ \phi\rightarrow\psi }[/math] | … | g,h |
| ⋮ | ⋮ | ⋮ | ⋮ |
| b | [math]\displaystyle{ \phi }[/math] | … | i,j |
| c | [math]\displaystyle{ \psi }[/math] | a,b MP或→E | g,h,i,j |
谓词逻辑
谓词逻辑增加一条规则：可以标示一个变量并开启一个子证明，记为 flag 某个体变项。
关于谓词逻辑的则增加以下规则。其中除要求 [math]\displaystyle{ \phi,\psi }[/math] 可以代入为任意公式外，还要求 [math]\displaystyle{ t }[/math] 是项且对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入， [math]\displaystyle{ a }[/math] 是个体变项且[math]\displaystyle{ a }[/math] 对 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中可自由代入。有时也可以直接使用 [math]\displaystyle{ t=x }[/math] 或 [math]\displaystyle{ a=x }[/math] 进行个体变项代入，但是由于存在混淆，建议避免。
- 全称量词消去（[math]\displaystyle{ \forall_E }[/math]，[math]\displaystyle{ \forall }[/math]-elim，US/UI）：从 [math]\displaystyle{ \forall x \phi }[/math] 可推出 [math]\displaystyle{ \phi[t/x] }[/math] ，其依赖假设不变。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ \forall x\phi }[/math] | … | c,d |
| b | [math]\displaystyle{ \phi[t/x] }[/math] | a ∀E | c,d |
- 存在量词引入（[math]\displaystyle{ \exists_I }[/math]，[math]\displaystyle{ \exists }[/math]-int，EG）：从 [math]\displaystyle{ \phi[t/x] }[/math] 可推出 [math]\displaystyle{ \exists x \phi }[/math] ，其依赖假设不变。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ \phi[t/x] }[/math] | … | c,d |
| b | [math]\displaystyle{ \exists x\phi }[/math] | a ∃I | c,d |
- 等词引入（[math]\displaystyle{ =_I }[/math]，[math]\displaystyle{ = }[/math]-int）：在任意地方，可以对任意项 [math]\displaystyle{ t }[/math] 得到 [math]\displaystyle{ t=t }[/math] ，不需要依赖任何假设。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ t=t }[/math] | =I |
- 等词消去（[math]\displaystyle{ =_E }[/math]，[math]\displaystyle{ = }[/math]-elim）：从 [math]\displaystyle{ s=t }[/math] 或 [math]\displaystyle{ t=s }[/math]，以及 [math]\displaystyle{ \phi[s/x] }[/math] 可以得到 [math]\displaystyle{ \phi[t/x] }[/math] ，其依赖假设为两者并集。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ s=t }[/math] | … | e,f |
| ⋮ | ⋮ | ⋮ | ⋮ |
| b | [math]\displaystyle{ \phi[s/x] }[/math] | … | g,h |
| ⋮ | ⋮ | ⋮ | ⋮ |
| c | [math]\displaystyle{ \phi[t/x] }[/math] | … | e,f,g,h |
然后的两条规则，涉及一个个体变项，需要要求结论或前提中不含有这一个个体变项，以保证这个变项本身的任意性。
- 存在量词消去（[math]\displaystyle{ \exists_E }[/math]，[math]\displaystyle{ \exists }[/math]-elim，ES/EI）：已经有 [math]\displaystyle{ \exists x \phi }[/math] (a) ，假设 [math]\displaystyle{ \phi[a/x] }[/math] (b) 成立并得到一个依赖 b 且不含有 [math]\displaystyle{ a }[/math] 的 [math]\displaystyle{ \psi }[/math] (c) ，则可以推出 [math]\displaystyle{ \psi }[/math] 且其依赖假设为两者并集中去除 b 。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ \exists x\phi }[/math] | … | e,f |
| b | [math]\displaystyle{ \phi[a/x] }[/math] | A (∃E) | b |
| ⋮ | ⋮ | ⋮ | ⋮ |
| c | [math]\displaystyle{ \psi }[/math] | … | b,g,h |
| d | [math]\displaystyle{ \psi }[/math] | a,b,c ∃E | e,f,g,h |
- 全称量词引入（[math]\displaystyle{ \forall_I }[/math]，[math]\displaystyle{ \forall }[/math]-int，UG）：已经有 [math]\displaystyle{ \phi[a/x] }[/math] 成立且其依赖的所有假设中均不含 [math]\displaystyle{ a }[/math] ，则可以推出 [math]\displaystyle{ \forall x\phi }[/math] ，其依赖假设不变。
| 行号 | 公式 | 规则 | 假设 |
|---|---|---|---|
| a | [math]\displaystyle{ \phi[a/x] }[/math] | … | c,d |
| b | [math]\displaystyle{ \forall x\phi }[/math] | a ∀I | c,d |
| 证明论 | |
|---|---|
| 形式化公理系统（形式化、公理化） | |
| 推理系统 | Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示 |
| Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎 | |
| Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算 | |
| 证明、演绎 | 演绎、可演绎、证明、可证明 |
| 命题、定理 | 公理/公理模式、定理、元定理、变形规则 |
| 推理规则性质 | 保存真实性、保存重言性 |
| 公理系统性质 | 可靠性、完备性/完全性、一致性、独立性 |