移出律

移出律
术语名称	移出律
英语名称
别名	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 化的理论基础，实现了从多元关系向一元关系序列的转换。

非经典逻辑中的情况

• 经典逻辑中移出律是可证明的定理。
• 同样接受移出律，其有效性不依赖于排中律，具有构造性解释。
• 多值逻辑和模糊逻辑：依赖蕴涵算子的定义。