The Coq mailing list

[croux AT andrew.cmu.edu]

The only problem with inductive predicates is if they admit so-called
Large Elimination: the ability to define a type by induction over the
possible proofs of the predicate. This is disallowed in Coq (try it!) and
therefore, the standard interpretation of Prop as a two-valued set is kept
consistent. In fact I believe it is standard procedure that every
modification of the logic implemented in Coq should be consistent with the
"folklore proof-irrelevant model". Sadly I'm not sure anyone has written
up such a model in detail. A combination of the Werner and Miquel paper:

The not so simple proof-Irrelevant model of CC (LNCS 2002)

and the article by Peter Dybjer:

Inductive Sets and Families in Martin-Löf's Type Theory and Their
Set-Theoretic Semantics

Is sufficient to piece together the full picture. However I agree that it
would be nice to see it all spelled out somewhere. If it has I am unaware
of it though.


Best,

Cody


> All these axioms are true in the usual set-theoretic proof-irrelevant
> models (in which Prop is the set 2, i.e., {0,1}).
> A nice, recent presentation is the 2011 LMCS paper by Lee and Werner:
>
> http://www.lmcs-online.org/ojs/viewarticle.php?id=675&layout=abstract
>
>
> I believe the Lee and Werner paper does not consider a system with
> inductive predicates -- i.e., what you
> get in Coq with
>
> Inductive ... : ... Prop := ...
>
> However, I doubt adding inductive predicates causes a problem. Someone can
> correct me if this is wrong.
> Also, if anyone knows of a presentation of CiC with inductive predicates
> and a set-theoretic proof-irrelevant model,
> I would be interested in knowing about it.
>
> Also, the Lee and Werner paper uses a system with judgmental equality.
> This differs from the type theory implemented in Coq,
> but I would be shocked if this difference would in any way make the
> conjunction of func_ext_dep, prop_ext and classic inconsistent.
>
> In summary: Yes, you should include them as axioms, because they are true.
>
> - Chad
>
>
> ________________________________
>  From: Math Prover 
> <mathprover AT gmail.com>
> To: 
> "coq-club AT inria.fr"
>  
> <coq-club AT inria.fr>
> Sent: Thursday, June 20, 2013 7:26 AM
> Subject: [Coq-Club] (soft question): Axioms: functional, prop, and
> classical
>
>
> Hi,
>
>   I'm referring to the axioms at http://coq.inria.fr/cocorico/CoqAndAxioms
>
>   I would like to use:
>
> == BEGIN ==
>
> Axiom func_ext_dep : forall (A:Type) (B:A->Type) (f g : forall x, B x),
>   (forall x, f x = g x) -> f = g.
>
> Axiom prop_ext : forall (P Q : Prop),
>   (P <-> Q) -> P = Q.
>
> Axiom classic : forall (P : Prop), P \/ ~ P.
>
> == END ==
>
>   as they would greatly simplify the proofs / tactics I'm using.
> However, I'm unsure if I can do this because:
>
> I don't know if:
>
> (1) the three above together is known to be consistent.
> (2) the three above together is known to be inconsistent.
> (3) neither (1) or (2) is known, but it's okay in the community to use
> all three together.
>
> By "okay" -- I mean if I were to submit a paper using the three axioms
> above, would people consider my proofs invalid because I used them.
> (In particular, I don't need them, but func/prop ext greatly
> simplifies rewrite rules.)
>
> Thanks!