Library Stdlib.Logic.ClassicalUniqueChoice

This file provides classical logic and unique choice; this is weaker than providing iota operator and classical logic as the definite descriptions provided by the axiom of unique choice can be used only in a propositional context (especially, they cannot be used to build functions outside the scope of a theorem proof)

Classical logic and unique choice, as shown in [ChicliPottierSimpson02], implies the double-negation of excluded-middle in Set, hence it implies a strongly classical world. Especially it conflicts with the impredicativity of Set.

[ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, Springer Verlag.

From Stdlib Require Export Classical.

Axiom
  dependent_unique_choice :
    forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
      (forall x : A, exists ! y : B x , R x y ) ->
      (exists f : (forall x:A, B x ), forall x:A, R x (f x)).

Unique choice reifies functional relations into functions

Theorem unique_choice :
forall (A B:Type) (R:A -> B -> Prop),
(forall x:A, exists ! y : B , R x y ) ->
(exists f:A ->B , forall x:A, R x (f x)).

The following proof comes from [ChicliPottierSimpson02]

From Stdlib Require Import Setoid.

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

Corollary not_not_classic_set :
((forall P:Prop, {P } + {~ P }) -> False ) -> False.

Notation classic_set := not_not_classic_set (only parsing).