24

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.

Mark Reitblatt
  • 1,690
  • 15
  • 20

1 Answers1

13

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.

Neel Krishnaswami
  • 32,528
  • 1
  • 100
  • 165
  • Thanks. And for impredicative Prop? – Mark Reitblatt Feb 14 '11 at 16:31
  • 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/ ) – Neel Krishnaswami Feb 14 '11 at 16:59