CODEWITHSUNDEEP
logicagdatype-theory
davik
davik

Reputation: 695

Law of excluded middle in Agda

I've heard the claim that Agda's Martin-Lof Type Theory with Excluded Middle is consistent. How would I go about adding it as a postulate? Also, after Adding LEM, is it then classical first-order logic? By this I mean, do I also have the not (for all) = there exist (not) equivalence? I don't know type theory, so please add additional explanation if you quote any results in type theory.

Upvotes: 3

Views: 1062

Answers (1)

gallais
gallais

Reputation: 12113

In MLTT, exists corresponds to a dependent pair which is defined in Data.Product in the standard library. It packages together the existence witness and the proof that it has the right property.

It is not necessary to postulate anything to prove that the negation of an existential statement implies the universal statement of the negated property:

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

To prove the converse however you do need the law of excluded middle to have a witness appear out of thin air. It is really easy to extend Agda with new postulates, you can simply write (Dec is defined in Relation.Nullary):

postulate LEM : (A : Set) → Dec A

It's always a good thing to remember how to prove double-negation elimination starting from LEM and we will need later on anyway so there it is (case_of_ is defined in Function and explained in README.Case):

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

And you can then prove that the negation of a universal statement implies an existential one like so:

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

Upvotes: 5

Related Questions