The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi Pierre,

> More generally, is the following set of declaration consistent with
> CIC + Classical ?
> 
> Parameter the : forall (A:Set)(P:A->Prop)
>               (E : exists a, P a)(U : forall a b, P a -> P b  -> a = b) , A.
> 
> Axiom the_ok : forall A P E U, P (the A P E U).
> Axiom the_eq : forall (A:Set) (P:A->Prop) E U a, P a -> a = the A P E U.

  First note that the_eq is superfluous (it is derivable).

  So, your question is about the consistency of having a definite
description operator.

  It is (presumably) consistent with the Set-predicative version of
classical CIC ("the" is interpreted as an oracle that "magically"
extracts an "effective" witness from a possibly non effective
(classical) proof). By the way, consistent definite descriptions was
the main motivation for moving Set to the predicative world.

  The operator "the" alone is inconsistent with the Set-impredicative
version of classical CIC. It can be used to derive a proof of
excluded-middle in Set (forall A:Prop, {A}+{~A}) from the assumption
of excluded-middle in Prop. Excluded-middle in Set is known to be
inconsistent with Set-impredicative CIC, as it allows to embed Prop in
bool:Set, hence to embed system U- in Coq, hence to derive a
contradiction (see e.g. file Hurkens.v, that you need to modify with
bool:Set and V:Set [this is the step that requires
Set-impredicativity]).

  As a remark, "the" and "the_ok" together are a (stronger) skolemized
form (for a codomain in Set) of what is called principle of definite
descriptions in the file ClassicalDescription.v of the current Coq
distribution. The latter implies the availability, in every Prop
context, of the excluded middle in Set (this is Chicli-Pottier-Simpson
paradox) which in turn allows to embed the inconsistent system U- in
the propositional part of Set-impredicative Coq.

  Hugo