上一页

ⓘ BHK释义




                                     

ⓘ BHK释义

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

                                     

1. 释义

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

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

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

                                     

2. 例子

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

无矛盾律 ¬ P ∧ ¬ P {\displaystyle \neg P\wedge \neg P} 被展开为 P ∧ P → ⊥) → ⊥ {\displaystyle P\wedge P\to \bot)\to \bot }:

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

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

在另一方面,排中律 P ∨ ¬ P {\displaystyle P\vee \neg P} 展开为 P ∨ P → ⊥ {\displaystyle P\vee P\to \bot} ,而一般没有证明。

                                     

3. 什么是荒谬?

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

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

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

                                     

4. 什么是函数?

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

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

                                     

5. 参见

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