21
$\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.

$\endgroup$
  • 6
    $\begingroup$ This sort of thing must get asked on the coq mailing list. $\endgroup$ – Andrej Bauer Feb 14 '11 at 7:50
  • 1
    $\begingroup$ Duh. For some reason this obvious venue slipped my mind. When you have a hammer... $\endgroup$ – Mark Reitblatt Feb 14 '11 at 16:31
  • 9
    $\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 Feb 14 '11 at 19:39
11
$\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.

$\endgroup$
  • $\begingroup$ Thanks. And for impredicative Prop? $\endgroup$ – Mark Reitblatt Feb 14 '11 at 16:31
  • 2
    $\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 Feb 14 '11 at 16:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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