Exercise 1.4.4 in A Course in Constructive Algebra.

Question

I am asking about Exercise 1.4.4 in A Course in Constructive Algebra by R. Mines et al.:

Let $I$ be the set of [infinite] binary sequences, and for each $i$ in $I$, let $A_i$
be $\{ x \in \{0, 1\} \mid x \geq i_j \ \text{for all} \ j \}$. Show that the natural mapping from $\Pi_i A_i$ to $A_0$ is onto if and only if WLPO

I am assuming that

1. $0$ denotes the sequence consisting of $0_n = 0$ for all $n$.
2. The natural mapping $\Pi_i A_i \rightarrow A_0$ is the projection $\pi_0$.

It is clear that $A_0 = \{ 0, 1 \}$ while $A_i \supset \{ 1 \}$ for all $i$.

$$ \lambda_i = 1 \\ \lambda'_0 = 0 \quad \text{and} \quad \lambda'_i = 1 \text{ for all } i \neq 0 $$

Then we would have $\pi_0(\lambda) = 1$ and $\pi_0(\lambda') = 0$, making $\pi_0$ onto.

This would have mean that the implication from the exercise is wrong. Since, WLPO is nonconstructive.

So, what is the problem?

---

Here WLPO refers to the following proposition:

If $\alpha$ is an infinite binary sequence, then either $\alpha_i = 0$ for all $i$; or it is impossible that $\alpha_i = 0$ for all $i$.

This is, from a constructive point of view, weaker than LLPO, which says that

If $\alpha$ is an infinite binary sequence, then either $\alpha_i = 0$ for all $i$; or $\alpha_i = 1$ for some $i$.

Answer 1

As I was writing up the question, I realized what the problem was, so I will write an answer right away:

The definition of $\lambda' : \Pi_i A_i$ is nonconstructive. An element of $\Pi_i A_i$ a rule which assigns to each $i \in I$, an element of $A_i$. (Otherwise, the projections $\pi_j : \Pi_i A_i \rightarrow A_j$ would become nonconstructive as well.)

For $\lambda'_i$, the rule is: If $i = 0$ then return $0$, otherwise return $1$. However, $I$ is not discrete; we cannot always decide whether $i = 0$ or not. In fact, deciding whether $i = 0$ or $\lnot (i = 0)$ is exactly what WLPO allows us to do. If we assume WLPO, then we may decide whether $i_j = 0$ for all $j$, or whether this is impossible. In the former case, set $\lambda'_i = 0$; in the latter, $\lambda'_i = 1$.

Conversely, if we had some $\lambda'$ such that $\pi_0(\lambda') = 0$. We can, given $i \in I$, calculate $\lambda'_i$. If $\lambda_i = 0$, then $0 \geq i_j$, or rather, $i_j = 0$ for all $j$. If $\lambda'_i = 1$, then it is impossible that $i_j = 0$ for all $j$. If this were the case, we would have $i = 0$ and $\lambda'_i = \lambda'_0 = 0$, which is a contradiction.