does countable choice survive booleanization?

does countable choice survive booleanization?

[Thomas Streicher]

Does anyone know an example of a a topos E with nno validating
internal countable choice (ICC), i.e. (-)^N preserves epis, such that
some booleanization of E doesn't validate (ICC) anymore?

In particular I am interested in the case where E is a relative
realizability topos induced by a pca A together with a sub-pca A_#.
For a particular such case I managed to answer the question positively
(see https://lmcs.episciences.org/4129/pdf) using a variant of Spector's
bar recursion. But I don't know the answer when I make the underlying
pca's of loc.cit. effective.
Another situation where I also don't know the answer is KV_{\neg_U\neg_U}
where KV is the Kleene-Vesley topos (see Jaap van Oosten's book) and U
is {\tau} where \tau decides the halting problem.

I think - or rather hope - that in these two latter cases
booleanization does not preserve (ICC). But for already quite some
time I failed to prove this.

Only recently I realized that I don't know any example where
booleanization does destroy (ICC). So I would be very glad to learn about
such an example.

Thomas



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: does countable choice survive booleanization?

[Thomas Streicher]

Alex Simpson has just told me that the answer to my question is simple:
all presheaf toposes validate ICC but certainly not all their booleanizations
since there are many boolean Groth. toposes not validating ICC.

Thank you Alex!

Alas, this doesn't answer the question for booleanizations of
generalized relative realizability toposes as e.g. the Kleene Vesley topos.

Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]