檢視 BHK釋義的原始碼

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

==釋義==

釋義精確的陳述一个予定的公式的證明是啥物。這是通過這个公式的佇結構頂懸歸納規定的：

* $ P \ wedge Q $ 的證明是有序嘿 < a , b >，遮的 a 是 P 的一个證明 b 是 Q 的一个證明。
* $ P \ vee Q $ 的證明是有序嘿 < a , b >，遮的 a 是零而且 b 是 P 的證明，抑是講 a 是一个爾 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 的證明變換做譀古的證明的函數。

譀古的標準例會當佇咧算術中揣著。假定零=一，閣進行數學歸納法：零=零通過等同公理得著；（歸納假設）若零等於特定自然數 n，著一將等於 n + 一 ( 皮亞諾公理：'''S'''m='''S'''n 若是唯一 m=n )，但是因為無=一，所以零嘛等於 n + 一；通過歸納，零等於任何數，所以任何兩个自然數攏是相等的。

所以乎，有對零=一的證明得著任何基本算數等式佮進而任何複雜算術命題的一種方式。進一步的講，會得著這種的結果，毋是必須的牽涉著皮亞諾公理零毋是任何自然數的後繼。這嘛予無代誌=一在 Heyting 算術（皮亞諾公理被重寫零='''S'''n → 零='''S'''零）適合充當 $ \ bot $。你這種零=一的使用驗證了爆炸原理。

==啥物是函數？==

BHK 釋義依賴佇咧制定共一个證明換做另外一个證明，抑是共一个域的元素變換做一个證明的函數的觀點。無仝版本的數學構造主義佇這點頂懸是有分歧的。

Kleene 可實現性理論這種函數看做是可計算函數。伊處理 Heyting 算術，遮的量化的域是自然數毋過原始命題有 x=y 彼个形體。x=y 的證明簡單是平凡的算法，若是 x 求值得著佮 y 求值仝款（伊對自然數總是會當決定的）， 無證明諾。會當通過歸納建造閣較複雜的算法。

==引用==

* Troelstra , A . " History of Constructivism in the Twentieth Century " . 一千九百九十一 . [一]
* Troelstra , A . " Constructivism and Proof Theory " . 兩千空三 . [二]

==參見==

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

[[分類: 待校正]]