219 views

Skip to first unread message

Jul 22, 2016, 3:32:47 PM7/22/16

to constructivenews

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

* 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

Jul 22, 2016, 5:27:18 PM7/22/16

to Martín Hötzel Escardó, constructivenews

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.

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.

Jul 23, 2016, 6:37:05 AM7/23/16

to constructivenews

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

Jul 23, 2016, 4:02:29 PM7/23/16

to constructivenews

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

I like the topological model disproving its provability.

Do you think this is even weaker than WCC?

Best,

Martin

Jul 24, 2016, 6:30:32 AM7/24/16

to constructivenews

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

Jul 24, 2016, 12:35:56 PM7/24/16

to construc...@googlegroups.com

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

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

—Toby

Jul 24, 2016, 3:56:02 PM7/24/16

to construc...@googlegroups.com

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

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

Jul 24, 2016, 4:05:24 PM7/24/16

to Hannes Diener, Constructive News

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.

http://www.math.ucla.edu/~joan/amsterdam2012handout.pdf

Jul 24, 2016, 4:41:48 PM7/24/16

to constructivenews

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

Jul 25, 2016, 5:39:58 AM7/25/16

to Toby Bartels, construc...@googlegroups.com, construc...@googlegroups.com

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

Bob

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

Jul 26, 2016, 2:37:25 AM7/26/16

to Andrew Swan, constructivenews

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

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

> --

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

Jul 28, 2016, 6:16:39 AM7/28/16

to Robert, Martín Hötzel Escardó, constructivenews

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.

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.

Jul 28, 2016, 1:36:17 PM7/28/16

to Robert, Martín Hötzel Escardó, constructivenews

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

Jul 29, 2016, 3:25:57 AM7/29/16

to Robert, Martín Hötzel Escardó, constructivenews

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

which unique choice holds. When B is empty, the choice principle I

proposed for discussion reduces to an instance of unique choice.

Best,

Martin

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu