The Coq mailing list

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

  Hi,

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

  With is_non_empty in Prop and single in Type as you defined them,
I'm tempted to believe in the consistency, since single, though in
Type, has no computational content (at least I see no evident reason
based on known paradoxes allowing to derive an inconsistency from your
axiom).

  However, is there any special reason why you don't define single in
Prop. If single were in Prop, your axiom would be (classically)
derivable. Alternatively, is there is any reason why you dont' define
is_nonempty in Type as just exhibiting a witness in X. By doing this,
your axiom would be derivable too (and moreover intuitionistically).

  Hope it helps.


> 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
> ..."?

  You're right, there is something missing here. This kind of
information is spread in various references, sometimes unpublished,
and should be collected in some common place.

   The original reference for models of pure Calculus of Constructions
is

  Th. Coquand. Metamathematical Investigations of a Calculus of
  Constructions. In P. Oddifredi, editor, Logic and Computer
  Science. Academic Press, 1990.

On the limits of induction schemata, see 

  Th. Coquand and C. Paulin-Mohring. Inductively defined types. In
  P. Martin-Löf and G. Mints, editors, Proceedings of Colog'88, volume
  417 of LNCS. Springer-Verlag, 1990.

For models of the pure Extended Calculus of Constructions with Prop
and Set distinguished, especially for classical logic in Prop combined
with a rich structure in Set, some tools and hints are in Alexandre
Miquel's papers (look at http://logical.inria.fr/~miquel for his PhD
Thesis or his LICS paper).

  You can also browse the Coq Logic library (look e.g. to Berardi.v
which shows that strong sums (or AC) + EM + impredicativity implies
proof-irrelevance) and the Rocq/PARADOXES user contribution (look
e.g. to Reynolds.v which shows that identifying bool and Prop is
inconsistent in the pure Calculus of Constructions).

  Hugo Herbelin

----------------------------------------------------------------------

(* (1) single defined in Prop *)

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

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

Lemma weak_choice : (X : Type) (is_nonempty X) -> (single X).
Intros; Apply NNPP.
Intro; Apply H.
Intro; Apply H0.
Split with [x:?]x==X0.
Intro; Apply (H1 X0); Reflexivity.
Intros; Rewrite H1; Rewrite H2; Reflexivity.
Qed.


(* (2) is_nonempty defined in Type *)

Definition is_nonempty := [X:Type]X.
Definition exists := [X:Type; P : X -> Prop](not ((x:X)(not (P 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)
}.

Just take single_prop := [x]x==x0 where x0:(is_nonempty X)