Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Excluded Middle for Type?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Excluded Middle for Type?


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Excluded Middle for Type?
  • Date: Tue, 02 Jul 2013 15:40:48 -0400

Such an axiom certainly breaks extraction, since it has no natural computational interpretation, but perhaps you don't care about extraction. It also makes Gallina "computation" highly non-computational, which also might not bother you, depending on the application. I don't know if it's logically consistent.

On 07/02/2013 03:38 PM, Chris Casinghino wrote:
I notice that, where the Coq FAQ discusses safe axioms, it mentions
excluded middle only for "Prop". This also seems to be the case in
the standard libraries.

Would it also be safe to add excluded middle for "Type"? That is,
could I add the following?

Inductive sum (A B : Type) : Type :=
| leftT : A -> sum A B
| rightT : B -> sum A B.

Axiom em_type : forall A : Type, sum A (A -> False).



Archive powered by MHonArc 2.6.18.

Top of Page