布劳威尔—海廷—柯尔莫哥洛夫解释

布劳威尔—海廷—柯尔莫哥洛夫解释通常简称为BHK解释，它通过证明陈述所需的构造来解释直觉主义逻辑的逻辑运算。它不只是为命题赋予真值，而是描述数学证明必须提供的证据：合取要求对两个分项分别给出证明，存在性陈述要求给出见证，而蕴含则要求给出一种转换证明的方法。其核心概念——构造与构造性证明——并未由这一解释本身完全定义。(mathematik.uni-muenchen.de)

历史背景

这一解释源于L. E. J. 布劳威尔对直觉主义数学基础的研究、阿伦德·海廷对其逻辑形式化的研究，以及安德雷·柯尔莫哥洛夫将逻辑视为问题演算的解释。海廷于1930年发表了他的形式化直觉主义演算；柯尔莫哥洛夫的《论直觉主义逻辑的解释》随后于1932年发表。(arxiv.org)

对柯尔莫哥洛夫而言，逻辑运算组织的是任务及其解答。解决 $A\land B$ 意味着解决两个任务；解决 $A\to B$ 意味着给出一种方法，将 $A$ 的解答转换为 $B$ 的解答。这与证明解释十分相近，但这一合称不应被理解为三人在哲学立场上完全一致：柯尔莫哥洛夫区分了问题与命题，并非简单地接受了布劳威尔的基础立场。(arxiv.org)

构造性解释条款

设 $A$ 和 $B$ 为命题， $D$ 为一个对象域。这一解释假定原子陈述所需的证据已经明确，并以递归方式解释复合陈述。其主要条款如下。(mathematik.uni-muenchen.de)

逻辑形式	所需的构造性证据
$A\land B$	一个有序对，由 $A$ 的证明和 $B$ 的证明组成。
$A\lor B$	其中一个分项的证明，同时注明被证明的是哪一个分项。
$A\to B$	一种构造，将 $A$ 的任意证明转换为 $B$ 的证明。
$\bot$	不存在证明； $\bot$ 表示矛盾。
$\neg A$	$A\to\bot$ 的证明，将假设给出的 $A$ 的证明转换为矛盾。
$\forall x\in D\,A(x)$	一种构造，对任意给定的 $d\in D$ ，都能生成 $A(d)$ 的证明。
$\exists x\in D\,A(x)$	一个有序对，包含见证 $d\in D$ 以及 $A(d)$ 的证明。

因此，合取保留了两份证据。析取不仅保留证据，也保留所作的选择： $A\lor B$ 的证明不能让究竟确立了哪一个选项悬而未决。蕴含通过作用于证明的构造性函数来理解，而不只是通过真值表来理解。这些解读也解释了逻辑的计算性描述中相应的积类型、和类型与函数类型。(pure.ed.ac.uk)

全称量词的条款要求有一种适用于任意输入的统一方法，而不只是断言每个实例都存在某个证明。存在量词的条款则要求同时给出一个对象，并验证该对象具有所声称的性质。例如，对于

\forall n\in\mathbb N\,\exists m\in\mathbb N\;(m>n)

可以用如下过程提供构造性证据：接收一个自然数 $n$ ，返回 $m=n+1$ ，并给出 $n+1>n$ 的初等证明。这同时展示了全称量词和存在量词的解释条款。(mathematik.uni-muenchen.de)

对经典原则的影响

排中律断言

A\lor\neg A.

按照BHK解释，要证明它的某个实例，就必须给出 $A$ 的证明或对 $A$ 的构造性反驳，并明确给出的是哪一种。仅凭逻辑形式本身，无法提供其中任何一种。因此，与经典逻辑不同，直觉主义逻辑不接受排中律作为不受限制的原则。但这并不妨碍在具备所需证据时证明排中律的特定实例。(pure.ed.ac.uk)

同样，双重否定消去，

\neg\neg A\to A,

也没有一般性的BHK构造。 $\neg\neg A$ 的证据会将对 $A$ 的反驳转换为矛盾，但并不会自动提供 $A$ 的证据。这一结论可由蕴含和否定的解释条款得出。相比之下， $A\to\neg\neg A$ 有一个直接的构造：给定 $A$ 的证明，将任何提出的反驳应用于该证明即可。(mathematik.uni-muenchen.de)

因此，构造性推理确实允许使用导出矛盾的论证。需要额外论证的是，把反驳的不可能性普遍当作构造所断言的对象或证明的替代手段。

自然演绎与证明计算

BHK证据与自然演绎的推理规则密切对应。合取引入构造一个证明对；合取消去则选取其中一个分项。蕴含引入把在某个假设下的推导转化为一种转换证明的操作，而蕴含消去——即肯定前件式——则将这一操作应用于其前提的证据。(pure.ed.ac.uk)

例如，

(A\land B)\to(B\land A)

的证明可以表示为如下操作：

\langle p,q\rangle\longmapsto\langle q,p\rangle.

这里，逻辑论证具有明确的计算行为：重新排列证据。证明规范化会消除不必要的引入—消去迂回步骤，例如先构造一个有序对，随即又选取其中一个分项。在这种计算对应关系下，这些简化对应于程序求值。(pure.ed.ac.uk)

类型论与应用

对于适当的逻辑系统和计算系统，柯里—霍华德对应使上述关系变得精确：命题对应于类型，证明对应于项，证明的简化对应于计算。合取对应于积类型，析取对应于带标签的和类型，蕴含对应于函数类型。量词则引出依赖类型，其中证据的类型可以依赖于输入或见证。(pure.ed.ac.uk)

不过，BHK并不等同于柯里—霍华德对应。BHK以构造性证据来解释意义；柯里—霍华德对应则在明确指定的演算之间建立对应关系。这些思想为类型论、证明助手和形式验证提供了支持。在这些领域中，数学陈述可以充当规约，而经过检查的项则可以作为满足这些规约的证据。(pure.ed.ac.uk)

适用范围与局限

BHK是一个解释意义的框架，其本身并不是一套定义完备的形式语义学。它并未解决有关构造的一些问题：哪些操作是允许的，如何确立这些操作的正确性，以及如何确定原子命题的证据。对蕴含的处理尤为重要，因为它涉及前提的所有可能证明，而不只是当前已知的证明。(mathematik.uni-muenchen.de)

可实现性解释通过明确规定实现公式的对象及这些对象上的操作，使相关思想具有数学形式。不能将其简单地等同于非形式化的BHK条款。关于这一解释形式化的研究探讨了应当如何理解构造性操作与语义后承；所提出的可实现性模型、范畴模型及其他模型，都包含了超出这些条款本身的额外选择。(pure.ed.ac.uk)

参考来源

Kolmogorov's Calculus of Problems and Its Legacyarxiv.org
Propositions as Typespure.ed.ac.uk
Mathematical semantics of intuitionistic logicarxiv.org