<p>Law of excluded middle does not make intuitionistic logic inconsistent; intuitionistic logic is in many regards a subset of classical logic (of course classical logic can't have proof objects and there are other diffrences). In Agda you can use the <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Postulates" rel="nofollow noreferrer">postulate</a> keyword for such things. The following could be added to your postulates.</p>

<p>$LEM : \{A : Set\} \to A \lor \neg A$</p>

<p>I was doing some proofs out of a book on first order logic where I found it more useful to have double negation elimination than LEM.</p>

<p>$\neg\neg E : \{A : Set\} \to \neg\neg A \to A$</p>

<p>One of course implies the other so take your pick.</p>

<p>edit:
One of your <a href="https://cstheory.stackexchange.com/questions/21836/why-does-coq-have-prop">previous questions</a> gives some insight here as well. cody made mention of Agda being predicative. Martin Lof type theory is predicative (as well as Agda which is basically MLTT). Agda still has large elimination and adding LEM does not make the logic inconsistent. Martin Lof originally tried to base MLTT off of System-F but its impredicative nature kept getting in the way of such things. This is part of the reason why MLTT is predictive.</p>

CC BY-SA 3.0
2014-12-24T06:32:32.160Z
BTW, do you have references to any articles which prove this?
Konstantin Solomatov
CC BY-SA 3.0
2014-12-24T06:46:35.880Z
Not off the top of my head but it is a well known fact. I tried looking for something briefly and couldn't find it. I'll try and get back with something later. If anyone else finds a reference please post it
Jake
CC BY-SA 3.0
2014-12-24T06:56:01.177Z
I found this: http://plato.stanford.edu/entries/logic-intuitionistic/ which says "Peano arithmetic PA comes from Heyting arithmetic HA by adding LEM". Which although is exactly what you asked for it is strong evidence that adding LEM to intuitionistic logic just gives something closer to classical logic.
Jake
CC BY-SA 3.0
2014-12-24T20:51:55.073Z
It might be worth noting that while Agda is Predicative, there is no *a priori* reason why the logic MLTT should be conservative over Heyting Arithmetic, which does not allow quantifying over functions. It is a non-trivial exercise that it does (see "Constructivism in Mathematics", chaper 10) **in the absence of universes**. With universes this does not hold. Nevertheless, adding EM to MLTT with universes is consistent (with ZFC), as the "usual" set-theoretic model validates it. I'm not certain the axiom of choice isn't necessary though.
cody
CC BY-SA 3.0
2014-12-26T20:04:10.773Z
Classical logic can have proof objects.
Andrej Bauer
CC BY-SA 3.0
2014-12-26T20:04:38.450Z
MLTT can be interpreted in classical set theory, therefore it is consistent to add excluded middle to it.
Andrej Bauer
CC BY-SA 3.0
2014-12-26T20:09:25.340Z
It seems different to me in the classical case. What construction would LEM have? It could be it's own unique thing I suppose but that is very different from what a constructivist would want in a proof object. I guess what im saying is that the idea of proof objects in classical logic must be different from what I understand proof objects to be.
Jake
CC BY-SA 3.0
2014-12-26T20:18:49.113Z
Or do you mean Gödel style proof strings. In tgat case yes I totally agree. I guess I should say you can't have BHK style proof objects
Jake
CC BY-SA 3.0
2014-12-27T01:10:03.230Z
I mean the computational interpretation of classical logic whereby we interpret Perice's law using `callcc`.
Andrej Bauer
CC BY-SA 4.0
2019-04-02T21:12:54.250Z
Note that we can, even in MLTT, prove `¬¬(A∨¬A)`. Additionally the functor `¬¬` is a modality, i.e. a monad with some additional properties. We can prove `return¬¬ : A → ¬¬A`, `map¬¬ : (A → B) → (¬¬A → ¬¬B)` and `join¬¬ : ¬¬¬¬A → ¬¬A`. I find this formulation, where using classical theory with LEM is similar to using the `IO` monad to incorporate side effects to be much more satisfying than postulating LEM for all types.
WorldSEnder
CC BY-SA 3.0
2014-12-24T04:40:23.883Z
2014-12-24T05:16:22.743Z
2017-04-13T12:32:28.117Z
Jake
<p>Adding LEM to MLTT is no problem. You simply need to assume a term of type <code>forall P:Prop, P \/ ~ P</code>. In Coq, you can use the LEM as follows:</p>

<pre><code>Require Import Classical_Prop.
Print classic.
</code></pre>

CC BY-SA 3.0
2014-12-24T06:33:31.070Z
It's about Prop but can we say the same about Set?
Konstantin Solomatov
CC BY-SA 3.0
2015-08-23T17:34:48.240Z
If you want it in set, just do `forall T:Set, T + (T -> False)`.
Konstantin Weitz
CC BY-SA 3.0
2014-12-24T01:45:39.823Z
2014-12-24T01:45:39.823Z
Konstantin Weitz
<p>A term that proves the excluded middle will have type:</p>

<p>$$ em:\forall T:\mathrm{Type},\ T\ +\ (T\rightarrow\bot)$$</p>

<p>In MLTT with universes, this can be seen as a kind of choice function, which picks an element from any non-empty type (or provides a proof of emptyness).</p>

<p>In the "usual" set-theoretic model (where function types are interpreted as the set-theoretic function spaces), $\mathrm{Type}$ is interpreted as some universe of sets, and $em$ can be given by invoking some version of the axiom of choice.</p>

<p>This shows that it is consistent to add such a term to "vanilla" MLTT, as it is validated in the set theoretic model.</p>

<p>In some versions of Agda, the set theoretic model cannot be built, in particular when <em>injectivity of type constructors</em> is assumed, for obvious reasons (such constructors are not necessarily injective in set theory!). And indeed, assuming $em$ is contradictory, as discussed in this fascinating exchange: <a href="https://lists.chalmers.se/pipermail/agda/2010/001565.html" rel="nofollow noreferrer">https://lists.chalmers.se/pipermail/agda/2010/001565.html</a>.</p>

<p>Note that there are weakened versions of $em$ which play more nicely with type theory, in particular those coming from Homotopy Type Theory, where EM is allowed only on "proof-irrelevant" types.</p>

CC BY-SA 3.0
2017-02-26T19:39:23.020Z
2017-02-26T19:39:23.020Z
cody
<p>Is it possible to add law of excluded middle to Martin-Löf type theory as an axiom? It seems to me, that it's possible to add it to Coq since Coq has a module for non-constructive reasoning. Also, it seems to be impossible to Agda since it leads to inconsistency. But can we add it to plain MLTT? And why it will/won't work?</p>

<lo.logic><type-theory><coq>
Law of excluded middle in MLTT
Konstantin Solomatov
# Law of excluded middle in MLTT

(Asked by: username_0 on 2014-12-23)

Is it possible to add law of excluded middle to Martin-Löf type theory as an axiom? It seems to me, that it's possible to add it to Coq since Coq has a module for non-constructive reasoning. Also, it seems to be impossible to Agda since it leads to inconsistency. But can we add it to plain MLTT? And why it will/won't work?

**Tags:** lo.logic, type-theory, coq


---

## 3 answers

### Answer by username_1 on 2014-12-24. Score: 7 | Accepted answer

Law of excluded middle does not make intuitionistic logic inconsistent; intuitionistic logic is in many regards a subset of classical logic (of course classical logic can't have proof objects and there are other diffrences). In Agda you can use the [postulate](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Postulates) keyword for such things. The following could be added to your postulates.

$LEM : \{A : Set\} \to A \lor \neg A$

I was doing some proofs out of a book on first order logic where I found it more useful to have double negation elimination than LEM.

$\neg\neg E : \{A : Set\} \to \neg\neg A \to A$

One of course implies the other so take your pick.

edit:
One of your [previous questions](https://cstheory.stackexchange.com/questions/21836/why-does-coq-have-prop) gives some insight here as well. username_2 made mention of Agda being predicative. Martin Lof type theory is predicative (as well as Agda which is basically MLTT). Agda still has large elimination and adding LEM does not make the logic inconsistent. Martin Lof originally tried to base MLTT off of System-F but its impredicative nature kept getting in the way of such things. This is part of the reason why MLTT is predictive.

> **Comments:**
> **username_0**: BTW, do you have references to any articles which prove this?  
> **username_1**: Not off the top of my head but it is a well known fact. I tried looking for something briefly and couldn't find it. I'll try and get back with something later. If anyone else finds a reference please post it  
> **username_1**: I found this: http://plato.stanford.edu/entries/logic-intuitionistic/ which says "Peano arithmetic PA comes from Heyting arithmetic HA by adding LEM". Which although is exactly what you asked for it is strong evidence that adding LEM to intuitionistic logic just gives something closer to classical logic.  
> **username_2**: It might be worth noting that while Agda is Predicative, there is no *a priori* reason why the logic MLTT should be conservative over Heyting Arithmetic, which does not allow quantifying over functions. It is a non-trivial exercise that it does (see "Constructivism in Mathematics", chaper 10) **in the absence of universes**. With universes this does not hold. Nevertheless, adding EM to MLTT with universes is consistent (with ZFC), as the "usual" set-theoretic model validates it. I'm not certain the axiom of choice isn't necessary though.  
> **username_3**: Classical logic can have proof objects.  
> **username_3**: MLTT can be interpreted in classical set theory, therefore it is consistent to add excluded middle to it.  
> **username_1**: It seems different to me in the classical case. What construction would LEM have? It could be it's own unique thing I suppose but that is very different from what a constructivist would want in a proof object. I guess what im saying is that the idea of proof objects in classical logic must be different from what I understand proof objects to be.  
> **username_1**: Or do you mean Gödel style proof strings. In tgat case yes I totally agree. I guess I should say you can't have BHK style proof objects  
> **username_3**: I mean the computational interpretation of classical logic whereby we interpret Perice's law using `callcc`.  
> **username_4**: Note that we can, even in MLTT, prove `¬¬(A∨¬A)`. Additionally the functor `¬¬` is a modality, i.e. a monad with some additional properties. We can prove `return¬¬ : A → ¬¬A`, `map¬¬ : (A → B) → (¬¬A → ¬¬B)` and `join¬¬ : ¬¬¬¬A → ¬¬A`. I find this formulation, where using classical theory with LEM is similar to using the `IO` monad to incorporate side effects to be much more satisfying than postulating LEM for all types.  

---

### Answer by username_5 on 2014-12-24. Score: 2

Adding LEM to MLTT is no problem. You simply need to assume a term of type forall P:Prop, P \/ ~ P. In Coq, you can use the LEM as follows:
Require Import Classical_Prop.
Print classic.

> **Comments:**
> **username_0**: It's about Prop but can we say the same about Set?  
> **username_5**: If you want it in set, just do `forall T:Set, T + (T -> False)`.  

---

### Answer by username_2 on 2017-02-26. Score: 1

A term that proves the excluded middle will have type:

$$ em:\forall T:\mathrm{Type},\ T\ +\ (T\rightarrow\bot)$$

In MLTT with universes, this can be seen as a kind of choice function, which picks an element from any non-empty type (or provides a proof of emptyness).

In the "usual" set-theoretic model (where function types are interpreted as the set-theoretic function spaces), $\mathrm{Type}$ is interpreted as some universe of sets, and $em$ can be given by invoking some version of the axiom of choice.

This shows that it is consistent to add such a term to "vanilla" MLTT, as it is validated in the set theoretic model.

In some versions of Agda, the set theoretic model cannot be built, in particular when *injectivity of type constructors* is assumed, for obvious reasons (such constructors are not necessarily injective in set theory!). And indeed, assuming $em$ is contradictory, as discussed in this fascinating exchange: <https://lists.chalmers.se/pipermail/agda/2010/001565.html>.

Note that there are weakened versions of $em$ which play more nicely with type theory, in particular those coming from Homotopy Type Theory, where EM is allowed only on "proof-irrelevant" types.


---

