Weak choice principles

[Alex Simpson <als@inf.ed.ac.uk>]

The recent discussion about real numbers in toposes has reminded
me of some questions I've previously wondered about concerning
choice principles in toposes.


As is well known, all that is needed to get the Cauchy reals
and Dedekind reals to coincide (and hence the Cauchy completeness
of the Cauchy reals) is N-N-choice (N being the natural numbers):

  (AC-NN)   (\forall n:N. \exists m:N. A(n,m)) \implies
                  \exists f:N->N. \forall n:N. A(n,f(n))

This is a very weak choice principle. Under classical logic
it is simply true (by the least number principle). Although
not provable intuitionistically, it is accepted
by the Bishop school of constructivism (in fact they accept
full dependent choice).


What I want to remark upon is that the coincidence of the Cauchy
and Dedekind reals also follows from the, apparently weaker,
principle of bounded choice:

  (AC-Nb)   (\forall n:N. \exists m \leq n. A(n,m)) \implies
                \exists f:N->N. \forall n:N. (f(n) \leq n) \and A(n,f(n))

from which one can derive, for any g:N->N

  (\forall n:N. \exists m \leq g(n). A(n,m)) \implies
           \exists f:N->N. \forall n:N. (f(n) \leq g(n)) \and A(n,f(n)).


Alongside this it is natural to consider a principle of boolean
choice:

  (AC-N2)   (\forall n:N. \exists m \leq 1. A(n,m)) \implies
                \exists f:N->N. \forall n:N. (f(n) \leq 1) \and A(n,f(n)).

(I am assuming 0 is a natural number). From (AC-N2) one can derive
for any k:N,

  (\forall n:N. \exists m \leq k. A(n,m)) \implies
           \exists f:N->N. \forall n:N. (f(n) \leq k) \and A(n,f(n)).


One obviously has implications

   (AC-NN)  ==>  (AC-Nb)  ==>  (AC-N2)

QUESTION 1  Can either of the above implications be reversed?

My conjecture is that they can't.


Regarding the relationship to the real numbers, as remarked above
we have:

   (AC-Nb)  ==>  R_C = R_D

where R_C and R_D are the Cauchy and Dedekind reals respectively.
In fact this implication cannot be reversed. More strongly:

   R_C = R_D  =/=>  (AC-N2)

QUESTION 2  Does (AC-N2) imply R_C = R_D?

Again, my conjecture is that it doesn't. Any counterexample here
would of course simultaneously show that (AC-N2) does not imply
(AC-Nb).


I'd be interested to hear if anyone has ideas on these questions, or
knows of references in which the above choice principles (other than
AC-NN) are discussed.

Thanks,

Alex Simpson


Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh
Email: Alex.Simpson@ed.ac.uk           Tel: +44 (0)131 650 5113
Web: http://www.dcs.ed.ac.uk/home/als  Fax: +44 (0)131 667 7209