Aquí es una manera diferente de ver que el principio en cuestión no es de manera constructiva demostrable. Vamos a razón de manera informal, de manera constructiva, y mostrar que el principio en la pregunta implica la menor limitada principio de la omnisciencia (LLPO).
LLPO: Para cualquier secuencia $a_0, a_1, \ldots$ de los números naturales tales que cada una de las $a_i$ es $0$ o $1$, y que en más de una $a_i$ es distinto de cero, el siguiente tiene: $a_{2i} = 0$ todos los $i$ o $a_{2i+1} = 0$ todos los $i$,
Porque LLPO no es constructiva válidos, este muestra que el principio no es constructiva válida.
Vamos a dejar que $G = (Z_2)^\omega$, una contables producto de $Z_2$ con sí mismo. Este grupo es generado por una secuencia $(g_i)$ de los elementos, que conmuta con cada uno de los otros, de tal manera que $g_i^2 = e$ por cada $i$. Un elemento típico de $G$ es de la forma $g_{i_1}\cdots g_{i_k}$ para algunos secuencia $i_1 < \cdots < i_k$ de los números naturales.
Deje $(a_i)$ ser una secuencia de números naturales cada uno de los cuales es $0$ o $1$. Vamos a proceder inductivamente. En la etapa de $2i$ si $a_{2i} = 0$, se pone en $H$ el elemento $g_i$ y también poner en el producto de $g_i$ con todos los elementos ya en $H$. En la etapa de $2i+1$ si $a_{2i+1} = 0$, se pone en $K$ el elemento $g_i$ y también poner en el producto de $g_i$ con todos los elementos ya en $K$. Tenga en cuenta que $H$ $K$ son decidable; para saber si un elemento $g_{i_1}\cdots g_{i_k}$ es en uno de ellos, sólo necesitamos examinar la secuencia $a_{i_1},\ldots, a_{i_k}$ y preguntar si contiene un elemento distinto de cero.
Debemos verificar $G = H \cup K$. Deje $g = g_{i_1}\cdots g_{i_k}$ ser un elemento de $G$. Por supuesto, en la mayoría de los una de las secuencia $a_{i_1},\ldots, a_{i_k}$ es distinto de cero (y el conjunto de los naturales es distinto de cero, por supuesto, un decidable conjunto). Si ninguno es cero, $g \in H$. Si el uno es de cero tiene un índice impar, $g \in H$. Si el uno es de cero tiene un índice, $g \in K$. Lo cierto es constructiva que cada número natural es par o impar, así que esto demuestra que $G = H \cup K$.
Por lo tanto, por el principio de la pregunta, $G = H$ o $G=K$.
Pero si afirmamos $G = H$, entonces podemos afirmar que el $g_i \in H$ todos los $i$, por lo que podemos afirmar que el $a_{2i} = 0$ todos los $i$. Del mismo modo, si afirmamos $G = K$ afirmamos $a_{2i+1} = 0$ todos los $i$. Que es lo que necesita para mostrar LLPO.
Esta construcción es el tipo de cosas que yo tenía en mente en mi otra respuesta como el "ejercicio computables álgebra", pero quizá es más fácil seguir cuando se escriben en términos de LLPO sin el desvío a la uniformización.
