什麼是P. Wadler類型命題中的「迂迴證明」？

在Propositions as Types，它寫的是：什麼是P. Wadler類型命題中的「迂迴證明」？

1935年，在25歲的時候，Gentzen15就不一一介紹，但邏輯自然演繹和相繼式的兩個新配方微積分是才被確立爲兩大用於制定邏輯的系統，直到今天仍然如此。他展示瞭如何規範化證明以確保他們不是「迴旋處」，產生了一個新的證明Hilbert系統一致性的證明。並且，爲了匹配Peano引入的存在量化符號「」的使用，Gentzen 引入了符號∀來表示通用量化。他寫出暗示爲A⊃B（如果A成立，則B成立），連詞A & B （A和B均成立），並且作爲A∨B（至少有一個A或B 成立）的結合。

什麼是迴旋證明？你能舉一個簡單的例子嗎？爲什麼這是一個問題？

來源

2016-01-22 jhegedus

我們來舉個例子：A ∧ B。

如果我們知道A和B，我們可以推斷出A ∧ B：

A B 
------- I 
A ∧ B

這就是所謂的介紹規則。

雙重，如果我們知道A ∧ B我們可以推斷出A，或B：

A ∧ B   A ∧ B 
------- E1  ------- E2 
    A    B

這些都是消除規則。

然後，如果我們知道A我們可以證明A作爲第一個使用引進規則推導A ∧ A，然後破壞它變成A（另有A），使用排除規則：

A A 
------- I 
A ∧ A 
-------- E1 
    A

而這種環島可能發生在更大的證據。

沒有理由做這個往返行程：我們結束了我們開始的地方！

連續微積分「禁止」排除規則後的引入規則。 Gentzen的結果表明，具有這個屬性的邏輯和引入規則之後的淘汰規則被允許的邏輯一樣強大。現在，這很重要，因爲證明的空間要小得多：首先我們消除（按照我們的需要製作小公式），然後引入（構建目標）。例如，對於自動證明搜索或程序合成，這實際上是有用的。

編輯這個答案的第一個版本具有A ∧ B證明：

A ∧ B   A ∧ B 
------- E1 ------- E2 
    A    B 
    ----------------- I 
     A ∧ B

然而，除了從直接證明：

A ∧ B

-------標識一個∧乙

它似乎是唯一的其他「簡單證明」。在Haskell語法一個這樣寫：

proof :: (a, b) -> (a, b) 
proof (x, y) = (x, y) 
-- or 
proof x = x 
proof = id

哪些是（除了嚴格的特性，其邏輯不感興趣）相同，並且唯一合理的定義。例如：

proof :: (a, b) -> (a, b) 
proof x = fst (x, x)

也是有效的，不再聰明瞭。

來源

2016-01-22 11:50:08 phadej

我已經做了這樣的證明已經太久了，所以我的生鏽的道歉。如果你在^消除之後不能使用^ -introduction，那麼你如何構造A^B？B^A的證明？ – MattClarke

@MattClarke謝謝！似乎我已經很長時間了，因爲我也觸及了這個話題。更正了答案 – phadej

什麼是P. Wadler類型命題中的「迂迴證明」？

回答

相關問題