Special case of countable choice

[Martín Hötzel Escardó]

Let's take countable choice in the following form:

* If every C(n) is inhabited, then the product of the sets C(n) is
inhabited.

Here C(n) is a set depending on a natural number n.

In the constructive setting I am interested in, this is undecided for arbitrary families C(n).

Now the sets C(n) I need to consider are of a very particular form, namely

** C(n) = A(n) + B

where

   ** The set A(n) is a subsingleton (any two of its elements are equal).

   ** The inhabitedness of A(n) is decidable.

   ** The set B is arbitrary.

   ** A(n) + B stands for the disjoint union of the two sets.

I don't believe countable choice for C(n) of this simple form is provable in my setting. But this does look much simpler than general countable choice.

If we have the A(n) component only (that is, B=0), then (*) holds. If the A(n) component is constant, then (*) holds too. But when we put them together we seem to get something non-trivial, although much simpler than choice.

Has any of you come across anything like this and/or have something interesting to say about this special case of countable choice?

Thanks,
Martin

[Robert]

Isn't your ** provable? Here's the element of the product. Go through A(0), A(1), etc, picking the unique element, until there is none, then pick a same element of B for the rest.

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.

[Andrew Swan]

This axiom follows from LPO, because we have a choice sequence if either A(n) is inhabited for all n, or empty for some n.

It also follows from the axiom of weak countable choice (WCC) from Bridges, Richman and Schuster, A Weak Countable Choice Principle. This is because, given C(n) as in (**), we can inductively define a new sequence of sets D(n) with at most one non singleton as below:

Take D(n) to be A(n) if A(m) is inhabited for all m <= n

Take D(n) to be B if A(n) is empty, but A(m) is inhabited for all m < n

Take D(n) to be {0} if A(m) is empty for some m < n

Then D(n) has at most one non-singleton, so we can apply WCC to get a choice sequence d(n) \in D(n).

Now apply induction again to get a choice sequence c(n) for C(n):

If A(n) is inhabited, take c(n) to be the unique element of A(n).

If A(n) is empty, take c(n) to be d(m) where m <= n is least such that A(m) is empty

However, I think this axiom fails in the topological model over the product of Cantor space with the unit interval, 2^N x [0,1]. Define A(n) to be a subset of {0} and B to be a subset of {0,1} as follows. Given a point (a, x) of the topological space, take A(n) to be equal to {0} if a(n) = 1 and empty otherwise. Take B to contain 0 iff for some n a(n) = 0 and x < 1/2 + 2^{-n}. Take B to contain 1 iff for some n a(n) = 0 and x > 1/2 - 2^{-n}. (And so if a(n) = 0 for some n and 1/2 - 2^{-n} < x < 1/2 + 2^{-n} then B = {0, 1}). Then I don't think there can be any choice sequence defined on any neighbourhood of the point (1, 1/2).

Best,

Andrew

[Martín Hötzel Escardó]

Thanks, Andrew, for the detailed answer.

I like the topological model disproving its provability.

Do you think this is even weaker than WCC?

Best,
Martin

[Andrew Swan]

It looks like your new axiom is even weaker than WCC.

That's because it seems that WCC fails in the topological model over the unit interval [0, 1]. We define a sequence of sets D(n) in the topological model where D(n) contains 0 on the interval [ 0, 1/2n ) and contains 1 on the interval ( 1/(2n + 1), 1 ]. Then D(n) is a singleton on [ 0, 1/(2n + 1) ) \cup ( 1/2n, 1 ]. So for n /= m, we can cover the unit interval with an open set where D(n) is a singleton and a open set where D(m) is a singleton. However, there's no choice function defined on any neighbourhood of 0, so WCC fails there.

However, if I recall correctly LPO holds in the topological model over [0, 1], so (**) does too.

Best,

Andrew

[Toby Bartels]

Bob wrote in part:

>Go through A(0), A(1), etc, picking the unique element, until there is none, then pick a same element of B for the rest.

The problem with this algorithm is that you wrote ‘pick a’ while recursing over the integers. A priori, that requires Dependent Choice. (If it had been another ‘pick the’, then that would have been fine.) You may object that there is at most one ‘pick a’ during the entire quantification, but that just reduces the requirement to WCC, as in Andrew's messages. (If it had been exactly one ‘pick a’, then that would have been fine.)


—Toby

[Hannes Diener]

So we could call Martin’s choice principle “delayed finite choice”.

Incidentally, what is (if there is any) the case against unique choice? In particular, would there be any reason to argue against unique choice on “low” types, such as the natural numbers?

Hannes

[Bas Spitters]

Unique choice fails in quasitoposes, so by assuming it we reduce the number of models.

In classical reverse mathematics unique choice blows up proof theoretic strength, IIRC, I could be wrong. I don't have the book handy now.

Joan also has a discussion (p10):
http://www.math.ucla.edu/~joan/amsterdam2012handout.pdf

[Martín Hötzel Escardó]

(In the constructive setting I am interested in, unique choice just holds. Martin)

[Robert]

So sorry to have filled the airwaves here with a false argument. Thanks to tToby for having figured out exactly where my mistake was.

Bob


----- Original Message -----

[Martin Escardo]

Thanks, Andrew, for the detailed answer.

I like the topological model disproving its provability.

Do you think this is even weaker than WCC?

Best,
Martin

On 23/07/16 11:37, Andrew Swan wrote:
> This axiom follows from LPO, because we have a choice sequence if either
> A(n) is inhabited for all n, or empty for some n.
>
> It also follows from the axiom of weak countable choice (WCC) from
> Bridges, Richman and Schuster, A Weak Countable Choice Principle

> <http://www.ams.org/journals/proc/2000-128-09/S0002-9939-00-05327-2/S0002-9939-00-05327-2.pdf>.

> --
> 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

> <mailto:constructivene...@googlegroups.com>.

[Robert]

At the risk of embarrassing myself even further, I wouldmlike to disagree with a statement below. It is claimed that if B is empty then Choice holds in this case. I am not convinced.

Suppose A(n) contains 0 if the nth Turing machine halts, and 1 if it does not. It is well known that one cannot prove this sequence has a choice sequence. The only open issue is whether the question of A(n) being inhabitedmis decidable. On the one hand, yes it is: there is a Turing machine that on each n answers yes. On the other hand, there may not be a way of producing a witness to A(n) being inhabited.

I'd say I'm just pointing out here some finer distinctions that could be made.

[Robert]

Before anyone else chimes in, let me say I have since become less convinced by my example. Internally, my A(n)s are not all inhabited. I was working with an unreasonable notion of "decidable ".

[Martin Escardo]

I have to point out (as I already did) that I am working in a system in
which unique choice holds. When B is empty, the choice principle I
proposed for discussion reduces to an instance of unique choice.

Best,
Martin