移出律
| 移出律 | |
|---|---|
| 术语名称 | 移出律 |
| 英语名称 | |
| 别名 | Exp, 输出律, 导出律, 柯里化规则 |
移出律(exportation, Exp)是命题逻辑的重要定理，指条件命题中合取和蕴涵之间的转化关系。一个前件为合取的条件命题，即表达给定几个条件可以推出对应结论的命题“如果 P 、 Q 则 R”，可以重新表述为一个后件为条件命题的条件命题，表达已经给定其中几个条件时，补充剩余条件就可以推出这一结论的命题“如果 P ，则如果 Q 则 R ”。
这与映射的 Curry 化有内在的相似性：对于多元映射，也可以给定其中某几个变量并定义从剩余变量出发的映射。
定理
以下重言式称为移出律(exportation)，通常简写为 Exp ： [math]\displaystyle{ \vDash ((P \land Q) \rightarrow R) \leftrightarrow (P \rightarrow (Q \rightarrow R)) }[/math]
按默认优先级和结合性，也可以写作 [math]\displaystyle{ \vDash (P \land Q \rightarrow R) \leftrightarrow (P \rightarrow Q \rightarrow R) }[/math]
该定理包含两个方向：
- 移出方向： [math]\displaystyle{ \vDash ((P \land Q) \rightarrow R) \rightarrow (P \rightarrow (Q \rightarrow R)) }[/math] ，将一个子条件“移出”命题前件。
- 移入方向： [math]\displaystyle{ \vDash (P \rightarrow (Q \rightarrow R)) \rightarrow ((P \land Q) \rightarrow R) }[/math] ，将一个子条件“移入”命题前件。
意义
- 在自然演绎系统中，移出律对应重要的推理规则：
- 移出规则：[math]\displaystyle{ (P \land Q) \rightarrow R \vdash P \rightarrow (Q \rightarrow R) }[/math]
- 移入规则：[math]\displaystyle{ P \rightarrow (Q \rightarrow R) \vdash (P \land Q) \rightarrow R }[/math]
- 在 Hilbert 系统中，移出律一般是一个定理。
- 移出律是命题的 Curry 化的理论基础，实现了从多元关系向一元关系序列的转换。
非经典逻辑中的情况
- 古典逻辑中移出律是可证明的定理。
- 同样接受移出律，其有效性不依赖于排中律，具有构造性解释。
- 多值逻辑和模糊逻辑：依赖蕴涵算子的定义。