アグダの排除された中間の法律

Question

私は、アグダのミドルを除いたマーティン・ロフ型理論が一貫しているという主張を聞いたことがあります。どのように私はそれを仮定として追加するつもりですか？また、LEMを追加した後は、古典的な一次論理ですか？これは私が意味するのは、私も（すべてのために）=存在していない（等しくない）等価性を持っていますか？私は型理論を知らないので、型理論の結果を引用するならば、さらに説明を加えてください。

Answer 1

MLTTでは、existsは、標準ライブラリのData.Productで定義されている従属ペアに対応します。それは存在証人とそれが正しい財産を持っているという証拠をパッケージ化します。

実存の文の否定は否定財産の普遍的な文を暗示していることを証明するために何かを仮定する必要はありません。

∄⇒∀ : {A : Set} {B : A → Set} → 
     ¬ (∃ λ a → B a) → 
     ∀ a → ¬ (B a) 
∄⇒∀ ¬∃ a b = ¬∃ (a , b) 

あなたがに排中律が必要なのですが、逆を証明するために目撃者は薄い空気の中に現れます。

postulate LEM : (A : Set) → Dec A 

それはLEMから始まる二重否定の除去を証明する方法を覚えておくことは常に良いことだと私たちは以下となります。あなたは、単に（DecがRelation.Nullaryで定義されている）を記述することができ、新しい公準とAgdaを拡張することは本当に簡単です。

¬¬A⇒A : {A : Set} → ¬ (¬ A) → A 
¬¬A⇒A {A} ¬¬p = 
    case LEM A of λ 
    { (yes p) → p 
    ; (no ¬p) → ⊥-elim $ ¬¬p ¬p 
    } 

そして、あなたはその後、ユニバーサル文の否定がそうのような 実存1を意味していることを証明することができます（case_of_はFunctionで定義され、README.Caseに説明されている）それは後でとにかくので、そこに必要があります。

¬∀⇒∃ : {A : Set} {B : A → Set} → 
     ¬ (∀ a → B a) → 
     ∃ λ a → ¬ (B a) 
¬∀⇒∃ {A} {B} ¬∀ = 
    case LEM (∃ λ a → ¬ B a) of λ 
    { (yes p) → p 
    ; (no ¬p) → ⊥-elim $ ¬∀ (¬¬A⇒A ∘ ∄⇒∀ ¬p) 
    } 

A gist with all the right imports