Agda中的排中律

Question

我听说过Agda的Martin-Lof类型理论与排中律是一致的。如何将其作为公设添加？此外，在添加LEM之后，它是否变成了经典的一阶逻辑？这意味着，我也有“非（对于所有）=存在（非）”等价关系吗？我不懂类型理论，请在引用类型理论结果时添加额外的解释。

- davik

Answer 1

在 MLTT 中，exists 对应于标准库 Data.Product 中定义的一个依赖对。它将存在证明和满足正确属性的证明打包在一起。

不需要假设任何东西来证明存在性陈述的否定蕴含了否定属性的普遍陈述。

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

然而，为了证明逆命题，您确实需要排中律才能让证人凭空出现。将Agda与新公设扩展非常容易，您可以简单地编写以下内容（Dec 在 Relation.Nullary 中定义）：

postulate LEM : (A : Set) → Dec A

记得如何从LEM开始证明双重否定消除总是件好事，而且我们以后会用到它，所以在这里提供（case_of_ 在Function中定义，在README.Case中解释）：

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

您可以通过以下方式证明普通陈述的否定蕴含着存在性陈述：

¬∀⇒∃ : {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)
    }

一个包含所有必要导入的代码片段

- gallais