排中律 · aiwiki.page

排中律是逻辑学中的一项原则，断言对任意命题 $P$ ，析取式 $P\lor\neg P$ 都成立：即 $P$ 或其否定成立。它在经典逻辑中有效，但直觉主义逻辑不接受它作为不受限制的原则。排中律涉及的是一个命题及其严格意义上的否定，而不是任意一对相互对立的选项。接受排中律，并不意味着每个命题的真假都能被查明或通过计算判定。(docs.lean-lang.org)

形式表述与经典解释

在命题逻辑中，排中律写作

P\lor\neg P.

其中， $\lor$ 表示相容析取， $\neg$ 表示否定。更准确地说，这一表达式是一个公理模式：用任意公式替换 $P$ ，就得到该原则的一个实例。根据所选的演绎系统，这些实例可以作为公理引入，也可以作为定理推导出来。这一模式也适用于经典一阶逻辑中含有量词的公式。(builds.openlogicproject.org)

在经典语义学中，每个命题都被赋予两种真值中的一种。否定将这一真值反转，而析取式只要至少有一个析取支为真，就为真。因此，排中律是一个重言式，如下列真值表所示：(builds.openlogicproject.org)

$P$	$\neg P$	$P\lor\neg P$
真	假	真
假	真	真

这确立了排中律在经典语义下的逻辑有效性，与 $P$ 的具体内容无关。但这并未分别确立任何一个析取支：对该析取式的证明，不一定能确定 $P$ 是否成立。(builds.openlogicproject.org)

历史背景

亚里士多德的《形而上学》第四卷第七章提出了一种影响深远的古代表述。亚里士多德认为，相互矛盾的断言之间不存在中间状态：对于一个主体，必须肯定或否定它具有某一属性。他在讨论中区分了矛盾关系与反对关系。例如，黑与白之间可以有中间色；而“是白的”与“不是白的”则是相互矛盾的选项，并非相互反对的两个极端。(classics.mit.edu)

传统的拉丁语表达 tertium non datur 意为“不存在第三种选择”。现代逻辑使用联结词和明确的演绎规则来表述这一原则，而不再仅仅使用属性及其对立面的语言。这种形式化使人们能够比较认可排中律的系统与不认可排中律的系统。(plato.stanford.edu)

与相关原则的区别

排中律应与二值原则区分开来。二值原则认为，每个命题都恰好具有真、假两种真值中的一种。二值原则是关于真值赋值的主张；排中律则是一个涉及否定与析取的公式。在经典解释下，两者密切相关，但在其他解释下，两者未必一致。例如，超赋值语义可以保留排中律公式，同时允许某些命题没有确定的真值。(plato.stanford.edu)

相比之下，不矛盾律表示为

\neg(P\land\neg P).

它排除了一个命题与其否定同时成立的情形。排中律则要求二者的析取成立。直觉主义逻辑认可不矛盾律，却不认可不受限制的排中律，这表明接受其中一项原则，并不一定需要接受另一项。(plato.stanford.edu)

排中律也不能为虚假两难提供依据。“这个物体是红色的或蓝色的”并不是排中律的实例，除非在相关论域中，“蓝色的”确实表示“不是红色的”。亚里士多德对矛盾关系与反对关系的区分已经涉及这一差别。(classics.mit.edu)

在数学证明中的作用

排中律通过穷尽所有情形的分类讨论来支持数学证明。要证明 $Q$ ，可以先证明 $P$ 蕴涵 $Q$ ，以及 $\neg P$ 蕴涵 $Q$ ，再利用 $P\lor\neg P$ 。在自然演绎中，最后一步是析取消去。分类讨论本身在直觉主义逻辑中也可使用；真正具有经典逻辑特征的步骤，是无需进一步论证就引入任意的排中律析取式。(leanprover.github.io)

以直觉主义逻辑为基础，不受限制的排中律与双重否定消去等价，后者表示为

\neg\neg P\rightarrow P.

假设排中律与 $\neg\neg P$ 成立。在 $P$ 成立的情形下，立即得到 $P$ ；在 $\neg P$ 成立的情形下，则得到矛盾，而直觉主义逻辑允许从矛盾推出 $P$ 。反过来，直觉主义推理可以证明 $\neg\neg(P\lor\neg P)$ ，再通过双重否定消去即可得到排中律。(docs.lean-lang.org)

这解释了排中律与经典反证法的联系：从 $\neg P$ 推导出矛盾，可以确立 $\neg\neg P$ ，而进一步得出 $P$ 则需要经典逻辑的这一步。相比之下，从 $P$ 推导出矛盾以证明 $\neg P$ ，在直觉主义逻辑中是合法的。(lipn.fr)

构造性解释与计算

按照布劳威尔—海廷—柯尔莫哥洛夫解释，一个析取式的证明必须提供其中一个析取支的证明，并指出究竟是哪一个。因此，不受限制的排中律就需要一种普遍的论证，说明如何在每个命题及其否定之间作出选择。直觉主义逻辑并不提供这样的论证。不过，当命题可判定时，它接受排中律的具体实例，例如某个指定的自然数是否为素数。(plato.stanford.edu)

无法证明不受限制的排中律，并不等于证明了它的否定。排中律的双重否定在直觉主义逻辑中是可证明的。这一区别关乎证明必须提供什么，而不仅仅关乎观察者目前是否知道答案。(lipn.fr)

在证明助手中，可以明确引入经典逻辑原则。Lean证明助手提供 Classical.em P，作为 $P ∨ ¬P$ 的证明。其文档区分了构造性推理与经典推理：借助经典逻辑获得这样的析取式，本身并不能提供适用于任意命题的可执行判定过程。(lean-lang.org)