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