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

Question

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?

Answer 1

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.