¿Implica el teorema de Tychonoff el principio de tercero excluido?

Question

Es bien sabido que usando el tercio excluido, podemos probar que el Teorema de Tychonoff implica el axioma de elección. Esto fue demostrado por Kelley en 1950.

Sin embargo, la prueba estándar requiere el tercio excluido en varios lugares. Por ejemplo, se requiere el tercio excluido para mostrar que la topología cofinita da un espacio compacto.

También es bien sabido que el axioma de elección implica la ley del tercio excluido.

La pregunta es: sobre una base intuicionista adecuada (como, por ejemplo, IZF), ¿implica el Teorema de Tychonoff la ley del tercio excluido? De manera equivalente, ¿implica el Teorema de Tychonoff el Axioma de Elección sobre una base intuicionista?

Edición: He avanzado hacia la respuesta. Es claro que el Teorema de Tychonoff implica una forma limitada de tercio excluido: que cualquier conjunto está vacío o no vacío. Esto no es exactamente la versión completa del tercio excluido que estamos buscando, que es que cada conjunto está habitado o vacío, pero es un paso en la dirección correcta.

Pues recordemos que podemos probar constructivamente que cualquier espacio compacto está habitado o no está habitado. También podemos probar constructivamente que el espacio vacío es compacto.

Consideremos un conjunto $Q$. Entonces para todo $x \in Q$, sabemos que $\emptyset$ es compacto. Por lo tanto, $S = \prod\limits_{x \in Q} \emptyset$ es compacto.

Ahora notemos que si $Q$ está vacío, entonces $S$ es el producto vacío, por lo tanto, habitado. Inversamente, si tenemos algún punto $x \in Q$, entonces $S \cong \emptyset$; por lo tanto, si $S$ está habitado, entonces $Q$ debe estar vacío. Así que $S$ está habitado si y solo si $Q$ está vacío. Dado que $S$ está o habitado o no, vemos que $Q$ está vacío o no.

Answer 1

Finalmente, di con la sorprendentemente simple idea necesaria para responder a esta pregunta de forma afirmativa. El teorema de Tychonoff de hecho implica ($\Delta_0$) el principio del tercero excluido de manera constructiva. Supongamos Tychonoff.

Lema: Para todas las familias $(A_i)_{i \in I}$ de conjuntos habitados, o bien existe o no existe una función de elección $\prod\limits_{i \in I} A_i$.

Prueba: Darle a cada $A_i$ la topología indiscernible. Formalmente, la topología indiscernible es el conjunto de todos los conjuntos $K \subseteq A_i$ tales que si $K$ está habitado, entonces $K = A_i$. La topología indiscernible en un espacio habitado es compacta (de hecho, es el mismo lugar que $1$). Por lo tanto, $\prod\limits_{i \in I} A_i$ está habitado o no, porque es compacto.

Corolario: se cumple el principio del tercero excluido ($\Delta_0$).

Prueba: basamos la demostración en la prueba de Diaconescu del tercero excluido desde la elección. Consideramos una proposición ($\Delta_0$) $P$, y definimos una relación de equivalencia $\sim$ en $\{0, 1\}$ por $x\sim y$ si y solo si $x = y \lor P$. Sea $I = \{0, 1\} / \sim$, y para $i \in I$, definimos $A_i = \{x \in \{0, 1\} \mid [x] = i\}$. Entonces cada $A_i$ está habitado, por lo que o bien existe o no existe una función de elección. Según Diaconescu, la existencia de una función de elección aquí es equivalente a $P \lor \neg P$. Por lo tanto, o bien $(P \lor \neg P)$, o bien $\neg (P \lor \neg P)$. Esto último es imposible.