Is constructive indefinite description a conservative extension?

Using Coq
1

Recall that the axiom of constructive indefinite description is given as

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

Let P : Prop be a proposition whose statement does not depend on the constructive_indefinite_description axiom. If P is provable using CID, does it follow that it was already provable without it?

My reason for suspecting this is that, in a context where proving P is our goal, we are already allowed to eliminate ex terms and build sig terms from their parts, so we ought not to actually need CID at any point. In any case where it seems like we do it may be that we just have to rearrange our proof to make sure our goal is in Prop at any time we need to eliminate an ex. But I’m not sure how to prove this (assuming it is even true).

2

Adding: my reason for wondering about this is that, if this is indeed a conservative extension, it suggests the possibility of a syntax extension allowing the declaration of sections within which we can define terms “as if” CID holds, but those terms are inaccessible outside the section unless their type is in Prop (or SProp) and expressible without reference to CID. The proof terms themselves would then be programmatically transformed to terms that do not use CID, to make them usable outside the section.

3

If P is provable using CID, does it follow that it was already provable without it?

No. For instance P := exists x : (type of CID), True. If this is provable without axioms, we also have a proof of CID. But it’s clearly provable using CID.

See also coq/theories/Logic/ChoiceFacts.v at 85755365f745426e8919c5a39fd0476e6bc9aa89 · coq/coq · GitHub and other theorems in this file

5

How do you get from a proof of exists x : CID, True to CID (where CID is the type of constructive_indefinite_description)? Note that CID is in Type so you can’t just destruct the existential.

Definition CID :=
  forall (A : Type) (P : A->Prop),
    (exists x, P x) -> { x : A | P x }.

Lemma ex_CID_to_CID : (exists x:CID, True) -> CID.
Proof.
  intro p.
  ...

What comes next?

6

Oh, that’s not what you’re saying. You’re saying the only way we could have a proof of exists x : CID, True is by first exhibiting a term of type CID. Which is of course true.

Never mind :confused: Thanks for the very straightforward answer.