The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Sat, 27 Aug 2011 13:20:17 +0200,
Pierre-Marie Pedrot 
<pierremarie.pedrot AT ens-lyon.fr>
 a écrit :

> > Parameter realize : forall {A:Type}, (A->Prop)->A.
> > Axiom realization : forall {A:Type} (P:A->Prop), (exists! x:A, P x)
> > -> P (realize P).
> 
> > (* Note that "unique existence (exists!)" is assumed instead of
> > "mere existence (exist).")
> 
> > What are expected dangers of assuming each?
> 
> This :
> 
> Lemma PHAIL : False.
> Proof.
> apply realize;intros [].
> Qed.
> 
> (Choice operator is inconsistent in Type Theory; you must assume
> that A is inhabited in realize, as :
> 
> Parameter realize : forall (A : Type), inhabited A -> (A -> Prop) ->
> A.
> 
> See the standard library Epsilon* modules for more informations.
> 
> PMP

I am not sure we can call it a choice operator.
For me a (naive?) version of a choice operator would rather be:

Axiom choice_operator:
 forall A (P: A -> Prop), (exists x, P x) -> {x | P x }.

which is fairly different (and nearer of the mathematical definition I
know) than the given one.

It is some kind of Prop elimination to type
(although the x in "exists x, P x" has no guarantee to be the same
as the x in "{x | P x}", unless we are in the case of unique choice)

I am pretty sure that this definition is already in the classical logic
part of coq (but I didn't browse it, to find in which module it lies).

And the operator I give is not known to be inconsistant in Type Theory.