<p>Actually, in section 4.5.3, he doesn't quite say that EM+impredicativity is inconsistent. He says that when you assume it, the model must becomes degenerately proof-irrelevant (the interpretation of all types other than Prop can  have at most one element). Andy Pitts describes a similar phenomenon <a href="http://www.cl.cam.ac.uk/~amp12/papers/nontpt/nontpt.ps.gz">"Non-trivial Power Types Can't Be Subtypes of Polymorphic Types"</a>. </p>

<p>For predicative versions of type theory, it's probably easier to just do the consistency proof than to Google for it -- universe stratification gives you everything you need for the simple-minded set-theoretic model of types (i.e., types are sets, terms are maps) to work out. Just observe that sets are closed under indexed sums and products, and get cozy with the axiom of replacement when interpreting universes. This is academic bad practice, of course, but the proof is still worth doing for yourself.</p>

CC BY-SA 2.5
2011-02-14T16:31:06.497Z
Thanks. And for impredicative Prop?
Mark Reitblatt
CC BY-SA 2.5
2011-02-14T16:59:04.933Z
Impredicative *Prop* makes no difference, since $2$ is a complete lattice, and you can interpret arbitrary intersections and unions with it. It's impredicative *Set* that complicates everything, since set-theoretic sets don't directly justify impredicative indexing. (C.f. Reynolds' "Polymorphism Is Not Set-Theoretic" http://www.springerlink.com/content/yn417gu033x85677/  )
Neel Krishnaswami
CC BY-SA 2.5
2011-02-14T09:56:10.347Z
2011-02-14T17:02:35.787Z
2011-02-14T17:02:35.787Z
Neel Krishnaswami
<p>I've seen (and heard) it claimed that it is safe to add the classical axiom of excluded middle to Coq, but I can not seem to find a paper supporting this claim. The papers I see listed on the <a href="http://coq.inria.fr/cocorico/TheoryBehindCoq">Coq wiki</a> about excluded middle are showing inconsistency with impredicative Set.</p>

<p>Indeed, it seems that Coquand states that adding Excluded Middle (an inhabitant of $A+\neg A$) is inconsistent for CoC in section 4.5.3 of his <a href="http://www.cs.chalmers.se/~coquand/meta.pdf">description</a>(PDF) of the metatheory of CoC. However, this section is a bit abstruse to me, so I may very well be misreading him.</p>

CC BY-SA 2.5
2011-02-14T07:50:47.663Z
This sort of thing must get asked on the coq mailing list.
Andrej Bauer
CC BY-SA 2.5
2011-02-14T16:31:35.480Z
Duh. For some reason this obvious venue slipped my mind. When you have a hammer...
Mark Reitblatt
CC BY-SA 2.5
2011-02-14T19:39:26.420Z
makes me happy that people think of posting here first, even for theory B questions that don't get enough attention :)
Suresh Venkat
<reference-request><lo.logic><coq>
Where is the proof that Coq + Excluded Middle is consistent
Mark Reitblatt
# Where is the proof that Coq + Excluded Middle is consistent

(Asked by: username_0 on 2011-02-14)

I've seen (and heard) it claimed that it is safe to add the classical axiom of excluded middle to Coq, but I can not seem to find a paper supporting this claim. The papers I see listed on the [Coq wiki](http://coq.inria.fr/cocorico/TheoryBehindCoq) about excluded middle are showing inconsistency with impredicative Set.

Indeed, it seems that Coquand states that adding Excluded Middle (an inhabitant of $A+\neg A$) is inconsistent for CoC in section 4.5.3 of his [description](http://www.cs.chalmers.se/~coquand/meta.pdf)(PDF) of the metatheory of CoC. However, this section is a bit abstruse to me, so I may very well be misreading him.

**Tags:** reference-request, lo.logic, coq

> **Comments:**
> **username_1**: This sort of thing must get asked on the coq mailing list.  
> **username_0**: Duh. For some reason this obvious venue slipped my mind. When you have a hammer...  
> **username_2**: makes me happy that people think of posting here first, even for theory B questions that don't get enough attention :)  

---

## 1 answers

### Answer by username_3 on 2011-02-14. Score: 13 | Accepted answer

Actually, in section 4.5.3, he doesn't quite say that EM+impredicativity is inconsistent. He says that when you assume it, the model must becomes degenerately proof-irrelevant (the interpretation of all types other than Prop can have at most one element). Andy Pitts describes a similar phenomenon ["Non-trivial Power Types Can't Be Subtypes of Polymorphic Types"](http://www.cl.cam.ac.uk/~amp12/papers/nontpt/nontpt.ps.gz).

For predicative versions of type theory, it's probably easier to just do the consistency proof than to Google for it -- universe stratification gives you everything you need for the simple-minded set-theoretic model of types (i.e., types are sets, terms are maps) to work out. Just observe that sets are closed under indexed sums and products, and get cozy with the axiom of replacement when interpreting universes. This is academic bad practice, of course, but the proof is still worth doing for yourself.

> **Comments:**
> **username_0**: Thanks. And for impredicative Prop?  
> **username_3**: Impredicative *Prop* makes no difference, since $2$ is a complete lattice, and you can interpret arbitrary intersections and unions with it. It's impredicative *Set* that complicates everything, since set-theoretic sets don't directly justify impredicative indexing. (C.f. Reynolds' "Polymorphism Is Not Set-Theoretic" http://www.springerlink.com/content/yn417gu033x85677/  )  

---

