24
$\begingroup$

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.

Improve this question
$\endgroup$
3
  • 6
    $\begingroup$ This sort of thing must get asked on the coq mailing list. $\endgroup$
    – Andrej Bauer
    Commented Feb 14, 2011 at 7:50
  • 1
    $\begingroup$ Duh. For some reason this obvious venue slipped my mind. When you have a hammer... $\endgroup$
    – Mark Reitblatt
    Commented Feb 14, 2011 at 16:31
  • 11
    $\begingroup$ makes me happy that people think of posting here first, even for theory B questions that don't get enough attention :) $\endgroup$
    – Suresh Venkat
    Commented Feb 14, 2011 at 19:39

1 Answer 1

Reset to default
13
$\begingroup$

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".

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks. And for impredicative Prop? $\endgroup$
    – Mark Reitblatt
    Commented Feb 14, 2011 at 16:31
  • 3
    $\begingroup$ 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 ) $\endgroup$
    – Neel Krishnaswami
    Commented Feb 14, 2011 at 16:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.