Is there a reverse mathematics of countable choice?

[Martin Escardo]

I am interested in determining the status of countable (dependent)
choice in constructive mathematics.

A number of theorems are proved using countable choice (which doesn't
hold in all models of intuitionistic logic of various kinds). How much
of countable choice do we get back from such theorems, if we assume them
and try to prove choice from them?

Martin

[Robert Lubarsky]

Does anybody have a suggestion as to what a fragment of CC might be? The few I've come across are choice for countable sequences of (non-empty) sets of natural numbers, and Richman's world's simplest axiom of choice (a single non-empty set with at most two elements). Also, a countable sequence such that, given any two elements of the sequence, (at least) one of them is a singleton.

Bob

--
You received this message because you are subscribed to the Google Groups "constructivenews" group.
To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Robert Lubarsky]

I assume you were actually asking about the implication <-. Because the implication -> is easy even without choice.

(In some detail: Let a_n be a binary sequence. Let x be -1/k if a_k is the first 1 in the sequence, 0 if there is no 1, to put it sloppily. Whether x is negative or not determines whether there is a 1 in the sequence.)

The right-to-left implication <- holds when every real is a Cauchy sequence (with a modulus of convergence). Which brings me to a particular instance of Martin's question which has interested me for a while: how much Choice does one need to show that the Cauchy reals = the Dedekind reals?

Bob


-----Original Message-----
From: Martin Escardo [mailto:escardo...@googlemail.com]
Sent: Tuesday, July 18, 2017 4:09 PM
To: Robert Lubarsky <lubarsk...@comcast.net>; construc...@googlegroups.com
Subject: Re: Is there a reverse mathematics of countable choice?

On 18/07/17 20:40, Martin Escardo wrote:
> But here I am more interested in facts about real numbers proved using
> countable (dependent) choice. One reason is Andrej's question in the
> HoTT mailing list asking whether we can prove that the reals are
> uncountable without countable choice. Another reason is a message and
> paper somebody else sent me, doing some things without countable
> choice, and other things with it, in a complex web of facts.

Here is an example: in the presence of countable (dependent) choice, we know that

(forall(x:R), x<0 \/ x>=0) <-> LPO.

Can this (specifically the implication ->) be proved without choice? If not, how much choice is needed for this?

(Alternatively, for the implication ->, we can ask how much of LPO one gets without choice. But this is a different question.)

Martin

[Martin Escardo]

On 18/07/17 20:19, Robert Lubarsky wrote:
> Does anybody have a suggestion as to what a fragment of CC might be? The few I've come across are choice for countable sequences of (non-empty) sets of natural numbers, and Richman's world's simplest axiom of choice (a single non-empty set with at most two elements). Also, a countable sequence such that, given any two elements of the sequence, (at least) one of them is a singleton.

I posted some such choice axioms implied by countable choice in this
list a while ago. (I can repeat them depending on how this discussion
develops.)

An example of such a "reversal" is given in a recent paper by Cory Knapp
and myself. I will formulate the facts without formulating the notions
(apologies). Using countable choice, we can show that a certain set of
subsingletons forms a "dominance" (the Rosolini dominance). Conversely,
assuming that they do form a dominance, we get some amount of choice
back. (The details are in the paper "partial elements and recursion in
univalent type theory", where the "univalentness" can be ignored for our
purposes.)

But here I am more interested in facts about real numbers proved using
countable (dependent) choice. One reason is Andrej's question in the
HoTT mailing list asking whether we can prove that the reals are
uncountable without countable choice. Another reason is a message and
paper somebody else sent me, doing some things without countable choice,
and other things with it, in a complex web of facts.

Best,
Martin

[Martin Escardo]

On 18/07/17 20:40, Martin Escardo wrote:

> But here I am more interested in facts about real numbers proved using
> countable (dependent) choice. One reason is Andrej's question in the
> HoTT mailing list asking whether we can prove that the reals are
> uncountable without countable choice. Another reason is a message and
> paper somebody else sent me, doing some things without countable choice,
> and other things with it, in a complex web of facts.

[Andrej Bauer]

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

[Andrew Swan]

The converse doesn't hold. The Cauchy reals and Dedekind reals are isomorphic in Lifschitz realizability, where AC(N, 2) fails.

Best,

Andrew

[Andrej Bauer]

Something like AC(N,2) limitted to semi-decidable total relations,
that might be possible to invert. (For the right definition of
"semidecidable").