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

釋義

編輯

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

  •  的證明是有序對<a,b>,這裡的a是P的一個證明而b是Q的一個證明。
  •  的證明是有序對<a,b>,這裡的a是0而b是P的證明,或者a是1而b是Q的證明。
  •  的證明是函數f: P→Q,它把P的證明變換成Q的證明。
  •  的證明是有序對<a,b>,這裡的a是S的一個元素,而b是φ(a)的一個證明。
  •  的證明是函數f: a→φ(a),它把S的一個元素a變換成φ(a)的證明。
  •  的證明被定義為 ,它的證明是把P的證明變換成 的證明的一個函數。
  •  是荒謬。應當沒有它的證明。

假定從上下文獲知原始命題的釋義。

例子

編輯

恆等函數是公式 的證明,不管P是什麼。

無矛盾律 被展開為 :

  •  的證明是函數f,它把 的證明變換成 的證明。
  •  的證明是證明的有序對<a,b>,這裡的a是P的證明,而b是 的證明。
  •  的證明是把P的證明變換成 的證明的函數。

把它們放置到一起, 的證明是函數f,它把有序對<a,b>變換成 的證明 -- 這裡的a是P的證明,而b是把P的證明變換成 的證明的一個函數。函數 證明了無矛盾律,不管P是什麼。

在另一方面,排中律 展開為 ,而一般沒有證明。

什麼是荒謬?

編輯

邏輯系統不可能有形式否定算子,使得在沒有P的證明的時候有正確的 非P的證明(參見哥德爾不完備定理)。BHK釋義轉而採納 非P為意味著P導致荒謬,指示為 ,所以¬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)適合充當 。這種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]

參見

編輯