BHK釋義

在數理邏輯中，直覺主義邏輯的布勞威爾-海廷-柯爾莫哥洛夫釋義（Brouwer–Heyting–Kolmogorov interpretation）或BHK釋義是由魯伊茲·布勞威爾、阿蘭德·海廷和獨立的由安德雷·柯爾莫哥洛夫提出的。它有時也叫做可實現性釋義，因為有關於史蒂芬·科爾·克萊尼的可實現性理論。

釋義

釋義精確的陳述一個給定的公式的證明是什麼。這是通過這個公式的在結構上歸納規定的：

$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求值同樣的數（它對於自然數總是可決定的），否則沒有證明。可以通過歸納建造起更複雜的算法。

引用

Troelstra, A. "History of Constructivism in the Twentieth Century". 1991. [1]
Troelstra, A. "Constructivism and Proof Theory". 2003. [2]