Some constructive versions of the Continuum Hypothesis are false. Are any true, or open?

Background

In constructive set theory (say based on CZF) there are inequivalent ways of stating the continuum hypothesis. Some of them are easily if not trivially refutable with common anti-classical assumptions. For instance:

Theorem: The class of all subsets of $\mathbb{N}$ is not in bijection with the class of all hereditarily transitive countable sets. (Clearly classically equivalent to ~CH)

Proof (CZF+REA+SC): The class of all hereditary transitive countable sets is a set. But the class of all subsets of N is a proper class (because SC: all sets are subcountable -- the anti-classical assumption). QED

But the same subcountability argument shows the class of all subsets of $\mathbb{N}$ is not in bijection with the set $2^\mathbb{N}$, nor with the set of real numbers. And anything that implies UZ (continuum is undecomposable) will imply that the set of real numbers is not in bijection with $2^\mathbb{N}$ either. So there are some classically equivalent but constructively inequivalent natural variants on CH there.

And of course CH can be rephrased without $\aleph_1$. We can ask whether there is a set which embeds into the continuum and into which the integers can be embeded, but neither converse holds. Constructively this is a weaker hypothesis, giving another "dimension" of natural variants.

It seems plausible to me that all of these variants are false under SC or UZ or intuitionistic continuity principle, or common assumption like that.

Question

Does anyone know of any simple statements that are classically equivalent but constructively inequivalent to CH, and which are true, or open problems, under common anti-classical assumptions like subcountability or unzerlegbarkeit?

-
I guess by "hereditarily transitive countable set" you just mean "countable ordinal"... –  Joel David Hamkins Jun 13 '10 at 17:40
You have to be quite careful about intuitionistic notion of "ordinal". For example, how would you show that a hereditarily transitive countable set is linearly ordered by $\in$? –  Andrej Bauer Jun 13 '10 at 18:14
I do. But it might also be something that splits into constructively inequivalent notions. --Dan –  Daniel Mehkeri Jun 13 '10 at 18:33
(Didn't see Andrej's comment) I wouldn't expect it to be linearly ordered. It supports transfinite induction though. --Dan –  Daniel Mehkeri Jun 13 '10 at 18:35
I see, thanks for the explanation. I hadn't realized that this concept splits intuitionistically. –  Joel David Hamkins Jun 14 '10 at 1:46

It is unclear to me what formulation of CH you have in mind that might make sense intuitionistically. Could you clarify that? I think I can still answer usefully the question about embeddings $\mathbb{Z} \to {?} \to \mathbb{R}$ which cannot be inverted intuitionistically.

By an embedding I mean an injective map $e$, i.e., $e(x) = e(y)$ implies $x = y$ for all $x$ and $y$ in the domain of $e$. (Incidentally, please please don't teach people that a map is injective or 1–1 when $x \neq y \implies e(x) \neq e(y)$, you're just making them addicted to negation, and it takes years to get rid of the habit.)

There is obviously a sequence of embeddings

$\mathbb{Z} \to \mathbb{Z}^\mathbb{N} \to \mathbb{R}$.

(I will leave it to you to find them.) There is no embedding from $\mathbb{Z}^\mathbb{N} \to \mathbb{Z}$ by the usual diagonalization argument. Classically, there is an embedding $\mathbb{R} \to \mathbb{Z}^\mathbb{N}$, but we cannot construct such an embedding intuitionistically. More precisely, Markov principle implies that such an embedding gives a decomposition of the reals. Since in the effective topos Markov principle is valid and the reals are indecomposable, intuitionistic logic alone cannot prove the existence of such an embedding.

Suppose $e : \mathbb{R} \to \mathbb{Z}^\mathbb{N}$ is an embedding. Because $e(0) \neq e(1)$, by Markov principle there exists $k$ such that $e(0)(k) < e(1)(k)$ or $e(0)(k) > e(1)(k)$. Let $t = \min(e(0)(k), e(1)(k))$ and consider the sets

$A = \lbrace x \in \mathbb{R} \mid e(x)(k) \leq t \rbrace$ and $B = \lbrace x \in \mathbb{R} \mid e(x)(k) > t \rbrace$.

They are inhabited, disjoint and their union is $\mathbb{R}$. Therefore $\mathbb{R}$ is decomposable. (It seems to me that we should be able to get rid of Markov principle in this argument.)

We cannot expect to show intuitionistically the stronger result, namely the existence of embeddings $\mathbb{Z} \to {?} \to \mathbb{R}$ such that intuitionistic logic proves that neither embedding can be reversed. That would consitute a proof of $\lnot CH$ which is classically valid and it would be quite surprising indeed.

-
To clarify, I have no one formulation of CH in mind. That's essentially the question. I am looking for just one formulation that can be proven. I know many can be refuted, but I already listed (non-exhaustively) quite a few combinations, and I don't mean to ask people here to try to refute them individually. I do mean it to be proven from indecomposability of reals, or other classically impossible assumption, because otherwise as you say it would also be classically valid proof. I don't mean to ask people here to prove ZF is inconsistent. –  Daniel Mehkeri Jun 15 '10 at 2:57
Ah, good! Nice question. –  Andrej Bauer Jun 15 '10 at 10:59
I also take it that V=L is not the sort of axiom you're looking for... –  Andrej Bauer Jun 15 '10 at 11:00
I don't know much about it. Is it ever used as an axiom in constructive mathematics? Also I understand V=L classically implies the axiom of choice. That in turn constructively implies EM. Do we know V=L doesn't constructively imply EM? –  Daniel Mehkeri Jun 15 '10 at 22:22
I think V=L needs unrestricted replacement, which is not regarded as constructive. –  arsmath Jan 3 '13 at 8:09
show 1 more comment