2つのものが等しくない場合、それらは等しくなりますか？

Question

Agdaの2つの値、または他の依存型言語では、v₁がv₂と等しくないことを証明できる場合、v₁はv₂と証明できますか？

同様に、((v₁ ≡ v₂ → ⊥) → ⊥) → v₁ ≡ v₂の機能がありますか？

v₁ ≡ v₂という値が1つしかないため、これは証明できない場合には公理として追加するのが安全なようです。

これは興味深い理由は、二重否定（(a → ⊥) → ⊥）がmonadを形成するということです。通常、そこから値を抽出することはできませんが、特定の値、たとえば⊥（それが古典的な論理モナドの矛盾を導いた場合、矛盾します）のようにすることができます。私は平等が抽出できるものかどうか疑問に思っていました。

Answer 1

AgdaまたはCoqでは法律が証明できないと思います。

大雑把に、私たちは、1つの仮説

(v1 = v2 -> False) -> False 

を持っていると我々は論文v1 = v2を証明する必要があります。

シークエンスベースのプルーフシステムでカットフリーの証明を考えてみましょう。最後のルールは何でしょうか？

そのタイプ（v1,v2は異なる変数である）はReflていないので、v1 = v2を導入することができません。

だから、それはH1が実際に証明可能である場合、すなわち

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

しかし、我々はまた、我々は

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

の派生元

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

を持っている必要があり、仮説の排除である必要があります

は、

と同等です

|- v1 = v2 -> False 

v1,v2についての他の前提なしでは明らかに証明できない。確かに、そうでない場合は、我々は明らかに間違っている

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

にそれを一般化できます。

一方、Agda/Coq/...は、提案された法律を意味する除外中立の法則と一致していると私は信じています。したがって、法律は一貫性に違反することはできません。

Answer 2

ここで提示されているように、直観主義型の理論では二重否定訂正は不可能ですが、その否定も不確かであるため、一貫して仮定できます。

しかし、古典的な公理はすべての型で証明可能ではありませんが、決定可能な型については証明可能です。決定可能なタイプは、証明可能生息したり無人島されるものである：Either A (A -> False)にだけパターンマッチ、と私たちはAを取得する場合、我々は終わった、としますDecidable A考える

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

、1はA上の二重否定の除去を実現することができますA -> Falseを取得し、(A -> False) -> Falseを適用してex falsoを使用します。

特別なケースとして、(a b : A) -> Decidable (a = b)の場合、((a = b -> False) -> False) -> a = bが証明可能です。 e。 Aには、決定的な平等があります。

継続モナドについては、このモナドの内部で作業するとき、ここでのモナド結合は「4倍」の否定排除に相当するので、古典的な推論の形式をとるので、not (not (not (not A))) -> not (not A))。 callCCも使用できます。Peirce's lawの別の古典的な文に相当します。

これについて興味深い見解があります：私たちは古典的な証明を取り、すべての命題をCont Falseに持ち上げます（言い換えれば、それらを二重否定する）。そして、元の命題の二重否定を証明する対応する建設的証明を得る。これは、命題とその二重否定が古典的に等価であるので、古典論理がモジュロ古典論理等価であることができるすべてを証明することができることを意味する。