如果兩件事並不相同，它們是否相等？

Question

如果Agda中的兩個值或某種其他依賴類型的語言可證明v₁不等於v₂，那麼您是否可以證明v₁等於v₂？

一樣，是有類型((v₁ ≡ v₂ → ⊥) → ⊥) → v₁ ≡ v₂的功能？

這似乎是安全的，如果它不能被證明是可以添加爲公理的東西，因爲最多可以有一個值爲v₁ ≡ v₂。

一個原因，這是有趣的是，雙重否定（(a → ⊥) → ⊥）形成monad。通常你不能從中提取數值，但是你可以使用某些值，比如⊥（如果你在經典邏輯monad中導出了一個矛盾，你就有矛盾）。我想知道平等是否可以提取。

Answer 1

我認爲法律不能在Agda或Coq中證明。

粗略地說，我們只有一個假設

(v1 = v2 -> False) -> False 

，我們需要證明的論斷v1 = v2。

考慮一個基於證據系統的證據。最後的規則是什麼？

它不能作爲v1 = v2的介紹，因爲Refl沒有那種類型（v1,v2是不同的變量）。

所以，它必須是假設的消除，即

H1: (v1 = v2 -> False) -> False |- v1 = v2 -> False 
H2: (v1 = v2 -> False) -> False , False |- v1 = v2 
--------------------------------------------------- (->E) 
(v1 = v2 -> False) -> False |- v1 = v2 

但是，如果H1確實證明的，我們也要有

(v1 = v2 -> False) -> False |- False 

從中我們得出

|- ((v1 = v2 -> False) -> False) -> False 

這相當於

|- v1 = v2 -> False 

如果沒有v1,v2的任何其他假設，這顯然是不可證明的。的確，否則我們可以推論到

|- forall v1 v2, v1 = v2 -> False 

這顯然是錯誤的。

在另一方面，我認爲，阿格達/勒柯克/ ...與排中的法，這意味着擬議中的法律相一致。因此，法律不能違反一致性。

Answer 2

否定之否定消除以直覺類型論無法證明，因爲陰氣這裏介紹的，但它的否定也是不可證明的，因此它可以持續承擔。

然而，雖然經典的公理是不可證明的所有類型，它們是可證明爲可判定的類型。可判定的類型是那些可證明居住或無人居住：

Decidable : Type -> Type 
Decidable A = Either A (A -> False) 

鑑於Decidable A，一個可以在A實現雙重否定排除：在Either A (A -> False)只是模式匹配，如果我們得到一個A，那麼我們就大功告成了，如果我們得到A -> False，然後我們申請(A -> False) -> False並且使用ex falso。

作爲特例((a = b -> False) -> False) -> a = b是可證明的，如果(a b : A) -> Decidable (a = b)，即i。即A具有可判定的平等性。

至於(A -> False) -> False延續單子，當我們在這個單子裏面工作時，我們得到某種形式的經典推理，因爲一元加入這裏對應於「四重」否定消除，所以not (not (not (not A))) -> not (not A))。我們也可以使用callCC，這對應於另一個經典語句Peirce's law。我們可以採取任何經典證明，將所有命題提升到Cont False（換句話說，雙重否定它們），並且我們得到相應的建設性證明，證明原始命題的雙重否定。這意味着構造邏輯可以證明經典邏輯能夠模仿經典邏輯等價，因爲命題及其雙重否定在經典上是等價的。