BHK释义
维基百科，自由的百科全书
在数理逻辑中，直觉逻辑的BHK 释义是由 L. E. J. Brouwer、Arend Heyting 和独立的由 Kolmogorov 提出的。它有时也叫做可实现性释义，因为有关于 Stephen Kleene 的可实现性理论。
目录 |
[编辑] 释义
释义精确的陈述一个给定的公式的证明是什么。这是通过这个公式的在结构上归纳规定的:
的证明是有序对 <a,b>，这里的 a 的 P 的一个证明而 b 是 Q 的一个证明。
的证明是有序对 <a,b>，这里的 a 是 0 而 b 是 P 的证明，或者 a 是 1 而 b 是 Q 的证明。
的证明是函数 f: P→Q，它把 P 的证明变换成 Q 的证明。
的证明是有序对 <a,b>，这里的 a 是 S 的一个元素，而 b 是 φ(a) 的一个证明。
的证明是函数 f: a→φ(a)，它把 S 的一个元素 a 变换成 φ(a)的证明。
的证明被定义为 
，它的证明是把 P 的证明变换成
的证明的一个函数。- 是荒谬。应当没有它的证明。
假定从上下文获知原始命题的释义。
[编辑] 例子
恒等函数是公式 
的证明，不管 P 是什么。
无矛盾律 
被展开为 
:
- 的证明是函数 f，它把
的证明变换成 的证明。 - 的证明是证明的有序对 <a,b>，这里的 a 是 P 的证明，而 b 是 的证明。
- 的证明是把 P 的证明变换成的证明的函数。
把它们放置到一起， 的证明是函数 f，它把有序对 <a,b> 变换成的证明 -- 这里的 a 是 P 的证明，而 b 是把 P 的证明变换成的证明的一个函数。函数 
证明了无矛盾律，不管 P 是什么。
在另一方面，排中律 
展开为 
，而一般没有证明。
[编辑] 什么是荒谬?
逻辑系统不可能有形式否定算子，使得在没有 P 的证明的时候有正确的 非 P 的证明(参见哥德尔不完备定理)。BHK 释义转而采纳 非 P 为意味着 P 导致荒谬，指示为，所以 ¬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) 适合充当。这种 0=1 的使用验证了爆炸原理。
[编辑] 什么是函数?
BHK 释义依赖于制定把一个证明变换成另一个证明，或者把一个域的元素变换成一个证明的函数的观点。不同版本的数学构造主义在这一点上是有分歧的。
Kleene 的可实现性理论把这种函数看成是可计算函数。它处理 Heyting 算术，这里的量化的域是自然数而原始命题有 x=y 的形式。x=y 的证明简单是平凡的算法，如果 x 求值得到与 y 求值同样的数(它对于自然数总是可决定的)，否则没有证明。可以通过归纳建造起更复杂的算法。
