The Coq mailing list

[Olivier Desmettre <olivier.desmettre AT inria.fr>]

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

Yes it is.  I checked your weak axiom of choice some days ago by
explicitely writing down the denotation in the standard omega-set
model of CIC.  Sorry for not having replied sooner...

Here follows the technical argument, whose underlying intuitions have
been already explained by Hugo in his previous mail.

If we forget Set, and consider the set-theoretical model of CIC
*without* Set (that is the naive model where propositions are
interpreted by booleans and where all propositional proof terms are
collapsed into a single non-informative object), the consistency of
your axiom is clear, because it is nothing else but the usual axiom of
choice of set-theory.

Now, if we consider Coq *with* Set in the omega-set model of CIC, it
is not sufficent to exhibit a set-theoretical object representing your
choice function (which is obvious), but we also have to exhibit a
realizer to show that this function is in the carrier of the
corresponding omega-set, that is a program (seen as some Gödel's code)
which represents the computational contents of your choice function.

However, your formulation is such that the target type (single X),
which is basically the sigma-type

  Sig P:(X->Prop).  (single_exists X P) * (single_single X P),

["Sig" denotes the strong sigma-type, not the propositional "Ex"]
is equipped with a full realizability relation (f.r.r), in the
sense that:

  for all x in the (carrier of the) interpretation of that type
  and for all program p, p realizes x in that type.

To check that the sigma-type (single X) has a f.r.r, we simply
have to remark that:

1. any propositional type has a f.r.r. (this is obvious for the full
   PER, but also for the empty PER because its carrier is empty,
   so we have nothing to check to ensure f.r.r. criterion!);

2. any sort (Prop, Type, Set) has a f.r.r (by definition of their
   realizability relation);

3. if (U x) has a f.r.r, for all x:T
   then (x:T)(U x) has a f.r.r.;

4. if T has a f.r.r., and
   if (U x) has a f.r.r. for all x:T,
   then Sig x:T. (U x) has a f.r.r.

   (same for the special case of the cartesian product T * U)

Intuitively, the f.r.r. criterion means that any program is as good as
any other program to represent the computational contents of a given
object of type (single X), or - which is equivalent - that the objects
of type (single X) have no computational contents, as already pointed
out by Hugo in his previous mail.

Going back to the syntax, it confirms the intuition that we cannot
build a non-constant function from (single X) to bool, simply because
we have no way to perform (non-trivial) case analysis on an object of
type (single X) - which has only one constructor - nor on its
components.

The interest of omega-sets equiped with a f.r.r. is that they behave
exactly as the ordinary sets, precisely because the information given
by the realizability relation is irrelevant.

In particular, it is easy to check that:

  if (U x) is an omega-set with a f.r.r. for all x of type T,
  then the product (x:T)(U x) in the category of omega-sets
  is nothing else but the set of *all* functions of the
  set-theoretical cartesian product, equipped with the f.r.r.

This remarks clearly solves the problem of the weak axiom of choice,
because it means that any set-theoretical choice function is also an
element of the carrier of the weak-choice-axiom omega-set, and
moreover, that any such function will be realized by any program.

Hope this helps,

-- Alexandre Miquel  
<miquel AT cs.chalmers.se>