Countable set in constructive mathematics

Question

Let $A$ be an alphabet (i.e. a set of symbols) and suppose that $A$ is countable.

Let $X$ be the set of all the words (i.e. finite strings) that I can write using the alphabet $A$.

Can I prove in constructive mathematics that $X$ is countable?

Answer 1

Yes, we can indeed prove this.

First, fix a particular bijection $f : \mathbb{N}^2 \to \mathbb{N}$. The usual construction works constructively.

Now use this to recursively construct bijections $f_j : \mathbb{N}^j \to \mathbb{N}$ for all $j \geq 1$. In particular, for $k \geq 1$, we define $f_{k + 1}(x_1, \ldots, x_k, x_{k + 1}) = f(f_k(x_1, \ldots, x_k), x_{k + 1})$. And of course we define $f_1(x) = x$.

Now consider strings over $\mathbb{N}$; let $\mathbb{N}^*$ be the set of such strings. Then we can explicitly define a bijection $g : \mathbb{N}^* \to \mathbb{N}$ by

$$g(x) = \begin{cases} 0 & x = \emptyset \\ f(f_k(x_1 x_2 \ldots x_k), k) + 1 & x = x_1 x_2 \ldots x_k, \; k > 0 \end{cases}$$

Therefore, $\mathbb{N}^*$ is countably infinite. In fact, we’ve explicitly constructed an enumeration of it.

Now fix an injection $i : A \to \mathbb{N}$. Then $i$ induces the injection $i^* : A^* \to \mathbb{N}^*$ defined by $i^*(x_1 x_2 \ldots x_k) = i(x_1) i(x_2) \ldots i(x_k)$. Then $g \circ i^* : A^* \to \mathbb{N}$ is an injection, so $A^*$ is countable.