# Where is the proof that Coq + Excluded Middle is consistent

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 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(PDF) of the metatheory of CoC. However, this section is a bit abstruse to me, so I may very well be misreading him.

• This sort of thing must get asked on the coq mailing list. Feb 14, 2011 at 7:50
• Duh. For some reason this obvious venue slipped my mind. When you have a hammer... Feb 14, 2011 at 16:31
• makes me happy that people think of posting here first, even for theory B questions that don't get enough attention :) Feb 14, 2011 at 19:39

• 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" springerlink.com/content/yn417gu033x85677 ) Feb 14, 2011 at 16:59