The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Dear Coq-Club

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. 

(Of course, adding an epsilon operator makes dec_P a "theorem" for any
P)

-- 
Gruß
Christian