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. [1]
• Troelstra, A. "Constructivism and Proof Theory". 2003. [2]

參見

• 直覺邏輯
• 直覺類型論
• 直覺主義
• 直覺類型論
• 經典邏輯
• 中間邏輯
• 線性邏輯
• 構造性證明
• Curry-Howard對應
• 可計算性邏輯
• 博弈語義