查看“︁移出律”︁的源代码

[[分类:命题逻辑定理]]{{DEFAULTSORT:yi2chu1lu:4}}
{{#seo:
|keywords=移出律,exportation,柯里化
|description=移出律是命题逻辑的重要定理，表明(P∧Q→R)与(P→(Q→R))逻辑等价。这一定理揭示了合取与蕴涵的深刻联系。在柯里霍华德同构中，是函数柯里化的逻辑学对应。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2025-11-25
}}
{{InfoBox
|name=移出律
|eng-name=exportation
|aliases=Exp,输出律,导出律,柯里化规则
}}
'''移出律'''('''exportation''', '''Exp''')是命题逻辑的重要定理，指条件命题中合取和蕴涵之间的转化关系。一个前件为合取的条件命题，即表达给定几个条件可以推出对应结论的命题“如果 P 、 Q 则 R”，可以重新表述为一个后件为条件命题的条件命题，表达已经给定其中几个条件时，补充剩余条件就可以推出这一结论的命题“如果 P ，则如果 Q 则 R ”。

这与映射的 [[Curry 化]]有内在的相似性：对于多元映射，也可以给定其中某几个变量并定义从剩余变量出发的映射。

== 定理 ==

以下重言式称为'''移出律'''('''exportation''')，通常简写为 '''Exp''' ：
<math>\vDash ((P \land Q) \rightarrow R) \leftrightarrow (P \rightarrow (Q \rightarrow R))</math>

按默认优先级和结合性，也可以写作
<math>\vDash (P \land Q \rightarrow R) \leftrightarrow (P \rightarrow Q \rightarrow R)</math>

该定理包含两个方向：
* 移出方向： <math>\vDash ((P \land Q) \rightarrow R) \rightarrow (P \rightarrow (Q \rightarrow R))</math> ，将一个子条件“移出”命题前件。
* 移入方向： <math>\vDash (P \rightarrow (Q \rightarrow R)) \rightarrow ((P \land Q) \rightarrow R)</math> ，将一个子条件“移入”命题前件。

== 意义 ==

* 在[[自然演绎系统]]中，移出律对应重要的推理规则：
** 移出规则：<math>(P \land Q) \rightarrow R \vdash P \rightarrow (Q \rightarrow R)</math>
** 移入规则：<math>P \rightarrow (Q \rightarrow R) \vdash (P \land Q) \rightarrow R</math>
* 在 [[Hilbert 系统]]中，移出律一般是一个定理。
* 移出律是命题的 Curry 化的理论基础，实现了从多元关系向一元关系序列的转换。

== 非经典逻辑中的情况 ==

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