The Coq mailing list

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

Hi,

> Assume the following:
> 
> X : Type
> P : X -> Prop
> 
> Given Coq/pCIC with no Axioms, I assume the meaning of 
> 
>         dec_P : "forall x : X , { P x } + { P x }"
> 
> is that one has constructed a decision procedure for the predicate P in
> pCIC, which implies Touring-decidability. Right?
> 
> If so, the question is, how many axioms may I add, without losing the
> meaning above.
> 
> In particular I'm interested in excluded middle,
> functional/propositional extensionality and, most important, choice.
> 
> I know that:
> 
>       choice -> (forall P , { P } + { ~ P } -> False) -> False ,
> 
> (cf. Coq.Logic.ClassicalUniqueChoice ) which together with classical
> implies:
> 
>       inhabited (forall P , { P } + { ~ P }) .
> 
> But fortunately this can only be eliminated at sort Prop, which does not
> seem to help in proving dec_P. 

You cannot prove dec_P but you will be able to use it in any
propositional context. By generalizing the proof of classic_set in
ClassicalUniqueChoice, you can indeed prove

  forall C:Prop, (forall P , { P } + { ~ P } -> C) -> C

then

  forall C:Prop, (forall x , { P x } + { ~ P x } -> C) -> C

Otherwise said, a proof of dec_P that is closed for some P over some X
in the context "choice, em, prop ext, fun ext" will indeed extract to
an axiom-free program from X to bool (though the correctness proofs
may use the axioms).

As far as I understand (but there are many people more knowledgable
than me on these matters), this is so because all of the axioms above
are purely propositional and therefore cannot directly contribute to a
necessarily-informative proof of { P x } + { ~ P x }. Indirectly, the
axioms could have contributed via the existing eliminations from
singleton types in Set/Type to Prop (this basically amounts to
eq_rect, False_rect and Acc_rect) but as they are presumably
consistent (thanks to the set-theoretical model of the predicative
Calculus of Inductive Constructions), eq_rect is realizable by the
identity, Acc_rect by a well-founded fixpoint and False_rect cannot
occur at all.

On the opposite side, in the proof of any propositional statement, you
will be able to rely on the existence of an oracle that "decides" the
provability of P, whatever P is actually decidable or not.

Hugo Herbelin