The Coq mailing list

[richard dapoigny <richard.dapoigny AT univ-smb.fr>]

Thanks Daniel for your answer. The problem is that i can loose 
decidability if i assume the description axiom: a sentence having form 
∀x, {P x} + {∼P x} does not mean that P is decidable, since it can be 
derived from excluded middle.


Le 27/08/2019 à 01:34, Daniel Schepler a écrit :
> On Mon, Aug 26, 2019 at 3:54 PM richard dapoigny
> <richard.dapoigny AT univ-smb.fr>
>  wrote:
> > Dear Coq users,
> >
> > Assuming classical logic with the following definitions:
> >
> > Variable object : Set. (* elements *)
> >
> > Definition eqobject := @Logic.eq object.
> >
> > Lemma eqobject_dec : forall x y:object, eqobject x y \/ ~(eqobject x y).
> > Proof.
> > intros x y;unfold eqobject;apply classic.
> > Qed.
> >
> > Is there a way to transform the following definition with Prop in classical 
> > logic (i.e., to remove booleans since left and right refer to sumbool):
> >
> > Definition Singleton (a:object) :=
> >    Caract
> >      (fun a':object =>
> >         match eqobject_dec a a' with
> >         | left h => True
> >         | right h => False
> >         end).
> >
> > Thanks for your help.
> If you also assume the constructive_definite_description axiom from
> the Description module, then you can construct classic_dec : forall P
> : Prop, {P} + {~P}.  This axiom is in line with traditional
> mathematics (but not with constructivist mathematics): it's a
> formalization of the type of definition that goes "define foo to be
> the unique x such that some condition holds on x".