BHK释义

在数理逻辑中，直覺主義邏輯的布勞威爾-海廷-柯爾莫哥洛夫释义（Brouwer–Heyting–Kolmogorov interpretation）或BHK释义是由魯伊茲·布勞威爾、阿蘭德·海廷和独立的由安德雷·柯爾莫哥洛夫提出的。它有时也叫做可实现性释义，因为有关于斯蒂芬·科尔·克莱尼的可实现性理论。

释义

释义精确的陈述一个给定的公式的证明是什么。这是通过这个公式的在结构上归纳规定的：

• ${\displaystyle P\wedge Q}$ 的证明是有序对<a,b>，这裡的a是P的一个证明而b是Q的一个证明。
• ${\displaystyle P\vee Q}$ 的证明是有序对<a,b>，这裡的a是0而b是P的证明，或者a是1而b是Q的证明。
• ${\displaystyle P\to Q}$ 的证明是函数f: P→Q，它把P的证明变换成Q的证明。
• ${\displaystyle \exists x\in S:\phi (x)}$ 的证明是有序对<a,b>，这裡的a是S的一个元素，而b是φ(a)的一个证明。
• ${\displaystyle \forall x\in S:\phi (x)}$ 的证明是函数f: a→φ(a)，它把S的一个元素a变换成φ(a)的证明。
• ${\displaystyle \neg P}$ 的证明被定义为${\displaystyle P\to \bot }$ ，它的证明是把P的证明变换成${\displaystyle \bot }$ 的证明的一个函数。
• ${\displaystyle \bot }$ 是荒谬。应当没有它的证明。

假定从上下文获知原始命题的释义。

例子

恒等函数是公式${\displaystyle P\to P}$ 的证明，不管P是什么。

无矛盾律${\displaystyle \neg (P\wedge \neg P)}$ 被展开为${\displaystyle (P\wedge (P\to \bot ))\to \bot }$ :

• ${\displaystyle (P\wedge (P\to \bot ))\to \bot }$ 的证明是函数f，它把${\displaystyle (P\wedge (P\to \bot ))}$ 的证明变换成${\displaystyle \bot }$ 的证明。
• ${\displaystyle (P\wedge (P\to \bot ))}$ 的证明是证明的有序对<a,b>，这裡的a是P的证明，而b是${\displaystyle P\to \bot }$ 的证明。
• ${\displaystyle P\to \bot }$ 的证明是把P的证明变换成${\displaystyle \bot }$ 的证明的函数。

把它们放置到一起，${\displaystyle (P\wedge (P\to \bot ))\to \bot }$ 的证明是函数f，它把有序对<a,b>变换成${\displaystyle \bot }$ 的证明 -- 这裡的a是P的证明，而b是把P的证明变换成${\displaystyle \bot }$ 的证明的一个函数。函数${\displaystyle f(\langle a,b\rangle )=b(a)}$ 证明了无矛盾律，不管P是什么。

在另一方面，排中律${\displaystyle P\vee (\neg P)}$ 展开为${\displaystyle P\vee (P\to \bot )}$ ，而一般没有证明。

什么是荒谬？

逻辑系统不可能有形式否定算子，使得在没有P的证明的时候有正确的 非P的证明（参见哥德尔不完备定理）。BHK释义转而采纳 非P为意味着P导致荒谬，指示为${\displaystyle \bot }$ ，所以¬P的证明是把P的证明变换成荒谬的证明的函数。

荒谬的标准例子可以在算术中找到。假定0=1，并进行数学归纳法：0=0通过等同公理得到；（归纳假设）如果0等于特定自然数n，则1将等于n+1 (皮亚诺公理：Sm = Sn当且仅当m = n)，但是因为0=1，所以0也等于n+1；通过归纳，0等于任何数，所以任何两个自然数都是相等的。

所以，有从0=1的证明得到任何基本算数等式和进而任何复杂算术命题的一种方式。进一步的说，要得到这种结果，不是必须的涉及皮亚诺公理0不是任何自然数的后继。这使得0=1在Heyting算术（皮亚诺公理被重写0=Sn → 0=S0）适合充当${\displaystyle \bot }$ 。这种0=1的使用验证了爆炸原理。

什么是函数？

BHK释义依赖于制定把一个证明变换成另一个证明，或者把一个域的元素变换成一个证明的函数的观点。不同版本的数学构造主义在这一点上是有分歧的。

Kleene的可实现性理论把这种函数看成是可计算函数。它处理Heyting算术，这裡的量化的域是自然数而原始命题有x=y的形式。x=y的证明简单是平凡的算法，如果x求值得到与y求值同样的数（它对于自然数总是可决定的），否则没有证明。可以通过归纳建造起更复杂的算法。

引用

• Troelstra, A. "History of Constructivism in the Twentieth Century". 1991.
• Troelstra, A. "Constructivism and Proof Theory". 2003.

参见

• 直觉逻辑
• 直觉类型论
• 直觉主义
• 直觉类型论
• 经典逻辑
• 中间逻辑
• 线性逻辑
• 构造性证明
• Curry-Howard对应
• 可计算性逻辑
• 博弈语义