命题逻辑中的形式演绎系统
摘要：在这节课中，我们将回顾形式演绎系统。解释这些系统如何用于解密逻辑表达式之间可能存在的关系，以及构建这些证明的基本元素：语言、公理和推理规则。这里提到了Łukasiewicz的公理，并解释了命题演算的演绎引擎 modus ponens。此外，还讨论了推理、定理和前提，并解释了在演绎系统中如何执行推理。
学习目标：
- 理解命题逻辑中形式演绎系统的概念。
- 识别形式演绎系统的基本组成部分。
- 了解命题演算中Łukasiewicz的公理。
- 理解modus ponens作为命题演算的演绎引擎。
- 理解演绎系统中如何执行推理以及前提、推理和定理之间的区别。
- 理解如何通过公理模式和推理规则生成推理。
- 认识逻辑连接表达式并用常用语言替换它们的能力。
内容目录:
什么是形式演绎系统？
命题逻辑中的Łukasiewicz公理
Modus Ponens：命题演算的演绎引擎
推理、定理和前提
如何在命题逻辑中进行证明？
证明等价性的概念
演绎(Meta)定理
演绎定理的逆定理
关于表达式的推理和关于推理的推理
单调性规则
对形式演绎系统和命题逻辑的综合思考
在我们对逻辑的研究中，我们已经到达了一个转折点，因为我们开始回顾命题逻辑的演绎系统。这是我们所见的一切开始变得操作性并且真正的逻辑精神开始显现的地方，因为我们将研究证明的本质。在这一点上，我们假设你已经了解如何编写表达式并理解命题逻辑的内容；如果你还不是很清楚，建议你复习之前的课程。
做完这些，接下来的是审视命题逻辑中的表达式如何相互关联以形成演绎。构建这些关系的机制是形式演绎系统。
什么是形式演绎系统？
形式演绎系统，或演绎计算系统，有三个基本组成部分：
- 一种形式语言。
- 一个公理模式。
- 基本推理规则。
我们已经回顾了所有与形式语言相关的内容。现在我们将介绍公理模式和基本推理规则。
为了构建命题演算的演绎系统，我们将从Łukasiewicz的公理开始构建演绎系统，基本推理规则我们将使用肯定前件法（Modus Ponens）。
Łukasiewicz的命题逻辑公理
如果 \alpha, \beta 和 \gamma 是命题演算的表达式，那么以下是命题演算的公理：
| [A1] | (\alpha \rightarrow (\beta \rightarrow \alpha)) |
| [A2] | ((\alpha \rightarrow (\beta \rightarrow \gamma))\rightarrow ((\alpha\rightarrow \beta)\rightarrow(\alpha \rightarrow \gamma))) |
| [A3] | ((\neg\beta \rightarrow \neg\alpha)\rightarrow(\alpha\rightarrow \beta)) |
肯定前件法：命题演算的演绎引擎
如果 \alpha 和 \beta 是命题演算的有效表达式， 那么肯定前件法规定，从 \alpha 和 (\alpha \rightarrow \beta) 可以推导出 \beta。以推理形式书写如下：
| (1) | \alpha | ; 前提 |
| (2) | (\alpha \rightarrow \beta) | ; 前提 |
| (3) | \beta | ; MP(1,2) |
这里使用“MP(1,2)”简写表示第(1)和第(2)步之间的肯定前件法，整个推理的综合表示为：
因此 \{\alpha, (\alpha \rightarrow \beta)\}\vdash \beta
我们很快就会看到，从Łukasiewicz的公理和肯定前件法出发，可以构建命题演算的所有演绎技巧，这些技巧综合了常规推理的基本规则，并为经典逻辑奠定了基础。
推理、定理和前提
在命题逻辑的演绎系统中进行的推理（或演绎）是一系列表达式的序列，其中每个表达式要么是一个前提，要么是仅使用Łukasiewicz的公理和肯定前件法从前提中得出的表达式。定理是无前提演绎的结果。前提可以是任何既不是公理也不是从公理推导出的表达式。一般来说，当我们有一组前提 \Gamma 和通过使用 \Gamma 中的某个元素、公理和肯定前件法得到的表达式 \alpha 时，写为 “\Gamma \vdash \alpha“，我们说
从 \Gamma 可推出\alpha
如果 \Gamma 是一个空集，那么我们不写作 “\emptyset\vdash \alpha” 而是写作 “ \vdash \alpha 。” 这表示 “\alpha 是一个定理”。这种表示定理的方式可以扩展到公理的表示，所以如果 \alpha、\beta 和 \gamma 是表达式，那么Łukasiewicz的公理可以写成以下形式
| [A1] | \vdash (\alpha \rightarrow (\beta \rightarrow \alpha)) |
| [A2] | \vdash((\alpha \rightarrow (\beta \rightarrow \gamma))\rightarrow ((\alpha\rightarrow \beta)\rightarrow(\alpha \rightarrow \gamma))) |
| [A3] | \vdash((\neg\beta \rightarrow \neg\alpha)\rightarrow(\alpha\rightarrow \alpha)) |
基于此，我们说公理是自明的陈述，或定理是从空白推断出的表达式，或者公理和定理是命题演算的性质。
命题逻辑中如何执行证明？
在这一点上，我们将停止讨论理论并转向实践。 关于执行证明可以说很多事情；但无论我们对演绎系统和命题逻辑说了多少精彩的话，且都被理解了，这并不意味着就一定能发展出执行证明所需的能力。因此，为了教授如何进行证明，我们将回顾一个简单定理的证明。
定理
如果 \alpha 是命题逻辑中的一个表达式，那么满足以下条件
\vdash (\alpha\rightarrow \alpha)
证明
| (1) | (\alpha\rightarrow ( \alpha \rightarrow \alpha)) | ; A1 |
| (2) | (\alpha\rightarrow ((\alpha\rightarrow \alpha)\rightarrow\alpha)) | ; A1 |
| (3) | ( (\alpha\rightarrow((\alpha\rightarrow\alpha)\rightarrow\alpha)) \rightarrow ((\alpha\rightarrow (\alpha\rightarrow\alpha))\rightarrow( \alpha\rightarrow \alpha))) | ; A2 |
| (4) | ((\alpha\rightarrow (\alpha\rightarrow\alpha))\rightarrow( \alpha\rightarrow \alpha)) | ; MP(2,3) |
| (5) | ( \alpha\rightarrow \alpha) | ; MP(1,5) |
因此 \vdash (\alpha\rightarrow\alpha)
证明结束。
正如可以看到的，在演绎系统和命题逻辑中，证明不是微不足道的，但一旦构建完成就容易复制。
现在，在我们开始使用这些技术进行推断之前，首先我们将发展一些对这项工作极其有用的属性和定义，因为如果我们只用这些进行推理，我们将遇到严重的问题。
证明等价性的概念
如果 \alpha 和 \beta 是任意表达式，并且 同时满足 \{\alpha\}\vdash \beta 和 \{\beta\} \vdash \alpha，那么我们说 \alpha 和 \beta 被证明是等价的，并写作 \alpha \dashv \vdash \beta。这可以符号化地概括为：
\left(\{\alpha\}\vdash\beta \wedge \{\beta\}\vdash\alpha \right) \Leftrightarrow \left(\alpha\dashv\vdash\beta\right)
这读作：从 \alpha 推出 \beta，且从 \beta 推出 \alpha 当且仅当 \alpha 和 \beta 被证明是等价的。
这是命题逻辑的一种元性质。
演绎（元）定理
如果 \alpha 和 \beta 是命题演算的表达式，且 \Gamma 是一组前提；那么如果从 \Gamma \cup \{\alpha\} 可以推导出 \beta，则意味着从 \Gamma 可以推导出 (\alpha \rightarrow \beta)。符号化表示为：
\left(\Gamma \cup \{\alpha\}\vdash \beta \right) \Rightarrow \left( \Gamma\vdash(\alpha\rightarrow\beta)\right)
证明：
为了满足 \Gamma \cup \{\alpha\}\vdash \beta，必须有以下形式的推导：
| (1) | \gamma_1 | ; \Gamma 的第1个前提 |
| \vdots | \vdots | |
| (n) | \gamma_n | ; \Gamma 的第n个前提 |
| (n+1) | \overline{\gamma}_1 | ; 之前某两行之间的肯定前件法 |
| \vdots | \vdots | |
| (n+m) | \overline{\gamma}_m | ; 之前某两行之间的肯定前件法 |
| (n+m+1) | \alpha | ; 前提 |
| (n+m+2) | \beta | ; 肯定前件法 (n+m+1, 其他之前的步骤，除了 n+m+1) |
因此 \Gamma\cup\{\alpha\} \vdash \beta
要使这成为可能，至少 \gamma_1, \cdots \gamma_n,\overline{\gamma_1},\cdots,\overline{\gamma_m} 中的一个表达式必须是 (\alpha\rightarrow \beta) 的形式，但所有这些行仅涉及 \Gamma 和 Łukasiewicz 公理的推导，因此必须满足 \Gamma\vdash (\alpha \rightarrow \beta)。因此证明了定理
证明结束。
演绎定理的逆定理
\left(\Gamma\vdash(\alpha \rightarrow \beta)\right) \Rightarrow \left( \Gamma \cup \{\alpha\}\vdash \beta \right)
证明：
如果满足 \Gamma\vdash (\alpha\rightarrow \beta)，则有以下形式的推导：
| (1) | \gamma_1 | ; \Gamma 的第1个前提 |
| \vdots | \vdots | |
| (n) | \gamma_n | ; \Gamma 的第n个前提 |
| (n+1) | (\alpha \rightarrow \beta) | ; 肯定前件法（在之前某两行之间） |
现在，如果我们将 \alpha 作为额外的前提添加到这个推理中，那么我们将有以下行：
| (n+2) | \alpha | ; 额外的前提 |
| (n+3) | \beta | ; MP(n+1,n+2) |
因此 \Gamma \cup \{\alpha\} \vdash \beta
这正是我们想要证明的。
证明结束。
关于表达式的推理和关于推理的推理
就像之前为了得到结果 \vdash (\alpha\rightarrow \alpha) 所做的演示那样，这些都是基于表达式的推导案例，因为每一步都包含了一个具体的表达式。类似地，也可以基于其他推导进行推导，其中每一步本身就是一次推导。在实践中，这两种方式的操作是相似的，但后者让我们能够利用演绎定理及其逆定理，从而大大增加了推理技巧的灵活性。为了展示这一点，让我们再次证明 \vdash (\alpha \rightarrow \alpha)，但这次使用推导而非表达式。其替代方案如下：
| (1) | \vdash (\alpha \rightarrow (\alpha \rightarrow \alpha)) | ; A1 |
| (2) | \{\alpha\}\vdash ( \alpha \rightarrow \alpha) | ; TD的逆(1) |
| (3) | \{\alpha\}\cup \{\alpha\}\vdash \alpha | ; TD的逆(2) |
| (4) | \{\alpha\}\vdash \alpha | ; 注意 \{\alpha\}\cup\{\alpha\}=\{\alpha\} |
| (5) | \vdash (\alpha\rightarrow \alpha) | ; TD(4) |
注意，这个推理并不比我们之前做的更短，但实现起来要容易得多，我们只需利用演绎定理、其逆定理和公理方案A1来构建证明。
乍一看，我们似乎只使用了Łukasiewicz的一个公理，并且忽略了其他公理和肯定前件法。这是否意味着通过这种方式推理，我们就忽视了其他公理和肯定前件法？答案是既是又不是。一方面，我们可以假装忽略了某些公理和肯定前件法，仅因为我们没有显式地使用它们，但必须记住，演绎定理及其逆定理正是基于Łukasiewicz的公理和肯定前件法而产生的，这意味着，正如我们在刚才的推理中所做的那样，使用它们实际上是在隐式地使用它们。
单调性规则
如果 \tau 是一个定理，那么对于任何表达式 \beta，将满足以下条件：
\{\beta\}\vdash\tau
这实际上是一个非常容易证明的规则，因为作为定理的 \tau 意味着 \vdash \tau。也就是说，存在一个推理，无需添加任何前提就能得到表达式 \tau，因此添加一个额外的表达式到（空的）前提中不会产生差异。
与此类似，可以提出以下结果：如果从一组前提 \Gamma 推出 \gamma，那么将满足以下条件：
\Gamma\cup\{\alpha\}\vdash\gamma
其中 \alpha 是任意表达式。
对演绎系统和命题逻辑的综合思考
当我们为命题逻辑语言提供一个推理规则和基本表达式时：肯定前件法和Łukasiewicz公理，我们所做的类似于构建一个“演绎机器”和提供“启动其运动的能量”。从这里开始，所有基本的演绎规则自然地开始涌现，并且我们将在这之后的部分中开始回顾。
还有一个细节。命题逻辑的表达式实际上是我们之前看到的两个符号语言的元表达式。请记住，这些元表达式的精妙之处在于，它们允许我们用任何语言的表达式替换它们的元变量，从而获得满足该结构的新表达式。当我们为命题逻辑语言提供公理模式和推理规则时，我们构建了命题逻辑的演绎系统，它允许生成连接表达式的推导。结果是我们拥有了一个能够包含无限推导的演绎框架：所有我们可以通过替换元变量为我们想要的表达式而获得的推导。当我们意识到不仅仅是我们一开始使用的那些两个符号语言的表达式，而是当我们代替使用我们通常语言的表达式时，逻辑的力量真正地被释放出来，因此我们对此感到惊奇。