On Wed, Jul 19, 2017 at 12:14 PM, Robert Lubarsky
<
lubarsk...@comcast.net> wrote:
> how much Choice does one need to show that the Cauchy reals = the Dedekind reals?
AC(N,2) suffices. Here 2 = {0,1} and AC(X,Y) is
∀ S ⊆ X × Y, (∀ x ∈ X ∃ y ∈ Y, S(x,y)) ⇒ ∃ f : X → Y ∀ x ∈ X, S(x, f x))
First note that AC(N,2) implies that, given any predicates P and Q on
N such that
∀ n, P(n) ∨ Q(n),
there is a choice function f : N → 2 such that
∀ n, (f(n) = 0 ∧ P(n)) ∨ (f(n) = 1 ∧ Q(n)).
Indeed, apply AC(N,2) to the relation S ⊆ N × 2 defined by S(n,b) ≡ (b
= 0 ∧ P(n)) ∨ (b = 1 ∧ Q(n)).
Given a real number x, use the above observation to obtain a function
f : Q × Q → 2 such that, for all q, r ∈ Q,
if q < r then
(f(n) = 0 ∧ q < x) ∨ (f(n) = 1 ∧ x < r).
We are now all set to obtain a Cauchy sequence converging to x by the
trisection method, where we consult f to see which way to go. That is,
starting from some rational bounds q_0 < x < r_0, define by recursion
the sequence n ↦ (q_n, r_n) by
(q_{n+1}, r_{n+1}) =
let s := (2 q_n + r_n) / 3
and t := (q_n + 2 r_n) / 3 in
if f(s,t) = 0 then (s, r_n) else (q_n, t)
I do not know how to invert this implication. I find it unlikely that
this can be done, since we instantiated S in AC(N,2) with a fairly
simple predicate (i.e., one that is no more complicated than < on R).
So a further weakening of AC(N,2) seems possible.
With kind regards,
Andrej