BHK释义

维基百科，自由的百科全书

在数理逻辑中，直觉逻辑的 Brouwer-Heyting-Kolmogorov 释义或 BHK 释义是由 L. E. J. Brouwer、Arend Heyting 和独立的由安德雷·柯爾莫哥洛夫提出的。它有时也叫做可实现性释义，因为有关于斯蒂芬·科尔·克莱尼的可实现性理论。

[编辑] 释义

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

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

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

[编辑] 例子

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

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

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

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

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

[编辑] 什么是荒谬?

逻辑系统不可能有形式否定算子，使得在没有 P 的证明的时候有正确的 非 P 的证明(参见哥德尔不完备定理)。BHK 释义转而采纳 非 P 为意味着 P 导致荒谬，指示为 $\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) 适合充当 $\bot$ 。这种 0=1 的使用验证了爆炸原理。

[编辑] 什么是函数?

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

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

[编辑] 参见

分类: 类型论 | 证明论 | 數理邏輯

See also ebooksgratis.com: no banners, no cookies, totally FREE.