Can you summarize the following document?
        
  釋義精確的陳述一個給定的公式的證明是什麼。這是通過這個公式的在結構上歸納規定的:  假定從上下文獲知原始命題的釋義。

  恆等函式是公式formula_10的證明,不管P是什麼。  無矛盾律formula_11被展開為formula_12: 把它們放置到一起,formula_12的證明是函式f,它把有序對變換成formula_8的證明 -- 這裡的a是P的證明,而b是把P的證明變換成formula_8的證明的一個函式。函式formula_23證明了無矛盾律,不管P是什麼。  在另一方面,排中律formula_24展開為formula_25,而一般沒有證明。

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

  BHK釋義依賴於制定把一個證明變換成另一個證明,或者把一個域的元素變換成一個證明的函式的觀點。不同版本的數學構造主義在這一點上是有分歧的。  Kleene的可實現性理論把這種函式看成是可計算函式。它處理Heyting算術,這裡的量化的域是自然數而原始命題有x=y的形式。x=y的證明簡單是平凡的演算法,如果x求值得到與y求值同樣的數(它對於自然數總是可決定的),否則沒有證明。可以通過歸納建造起更復雜的演算法。
在數理邏輯中,直覺主義邏輯的布勞威爾-海廷-柯爾莫哥洛夫釋義(Brouwer–Heyting–Kolmogorov interpretation)或BHK釋義是由魯伊茲·布勞威爾、阿蘭德·海廷和獨立的由安德雷·柯爾莫哥洛夫提出的。它有時也叫做可實現性釋義,因為有關於斯蒂芬·科爾·克萊尼的可實現性理論。