The Coq mailing list

[Chad E Brown <cebrown2323 AT yahoo.com>]

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!