The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

Hi. Would it be consistent (including consistency with
existence of the sort Set) to assume the following weak
axiom of choice?

Require Classical_Type.
Require Sets.
(** etc **)

Definition is_nonempty := [X:Type]((X->False) -> False).
Definition exists := [X:Type; P : X -> Prop](not ((x:X)(not (P x)))).

(** (single X) is the type of singleton subsets of X **)

Record single [X : Type] : Type := {
single_prop : X -> Prop ;
single_exists : (exists X single_prop);
single_single : (x,y: X)(single_prop x) -> (single_prop y) -> (x == y)
}.


Axiom weak_choice : (X : Type) (is_nonempty X) -> (single X).


One wouldn't, on the other hand, assume the "axiom of dependent choice"
because then this would be equivalent to the usual axiom of choice.


More generally is there a good reference to look at to understand
how to answer questions of the form "would it be consistent to assume
..."?


Thanks---
Carlos Simpson