# Does Tychonoff's Theorem imply Excluded Middle?

It is well-known that using excluded middle, we can prove that Tychonoff's Theorem implies the axiom of choice. This was proved by Kelley in 1950.

However, the standard proof requires excluded middle in several places. It requires excluded middle to show that the cofinite topology gives a compact space, for example.

It is also well-known that the axiom of choice implies the law of excluded middle.

The question is: over a suitable intuitionist foundation (such as, for example, IZF), does Tychonoff's Theorem imply the law of excluded middle? Equivalently, does Tychonoff's Theorem imply the Axiom of Choice over such a foundation?

Edit: I've made some progress towards the answer. It is clear that Tychonoff's Theorem implies a limited form of excluded middle: that any set is either empty or non-empty. This is not quite the full version of excluded middle we're looking for, which is that every set is either inhabited or empty, but it is a step in the right direction.

For recall that we can prove constructively that any compact space is either inhabited or not inhabited. We can also prove constructively that the empty space is compact.

Consider some set $$Q$$. Then for all $$x \in Q$$, we know that $$\emptyset$$ is compact. Therefore, $$S = \prod\limits_{x \in Q} \emptyset$$ is compact.

Now let us note that if $$Q$$ is empty, then $$S$$ is the empty product, hence inhabited. Inversely, if we have some point $$x \in Q$$, then $$S \cong \emptyset$$; thus, if $$S$$ is inhabited, then $$Q$$ must be empty. So $$S$$ is inhabited if and only if $$Q$$ is empty. Since $$S$$ is either inhabited or not, we see that $$Q$$ is either empty or not.

• Thanks for pointing out my error. When reading and thinking about your question, I conflated "non-empty" and "inhabited". So I humbly retract my answer. Aug 11, 2022 at 18:33

At long last, I hit on the surprisingly basic insight needed to answer this question in the affirmative. Tychonoff’s theorem does indeed imply ($$\Delta_0$$) excluded middle constructively. Assume Tychonoff.
Lemma: For all families $$(A_i)_{i \in I}$$ of inhabited sets, there either is or is not a choice function $$\prod\limits_{i \in I} A_i$$.
Proof: give each $$A_i$$ the indiscrete topology. Formally, the indiscrete topology is the set of all sets $$K \subseteq A_i$$ such that if $$K$$ is inhabited, then $$K = A_i$$. The indiscrete topology on an inhabited space is compact (in fact, it’s the same locale as $$1$$). Thus, $$\prod\limits_{i \in I} A_i$$ is either inhabited or not, because it is compact.
Corollary: the ($$\Delta_0$$) law of excluded middle holds.
Proof: we base the proof on Diaconescu’s proof of excluded middle from choice. Consider some ($$\Delta_0$$) proposition $$P$$, and define an equivalence relation $$\sim$$ on $$\{0, 1\}$$ by $$x\sim y$$ iff $$x = y \lor P$$. Let $$I = \{0, 1\} / \sim$$, and for $$i \in I$$, define $$A_i = \{x \in \{0, 1\} \mid [x] = i\}$$. Then each $$A_i$$ is inhabited, so there either is or isn’t a choice function. As per Diaconescu, the existence of a choice function here is equivalent to $$P \lor \neg P$$. Thus, either $$(P \lor \neg P)$$, or $$\neg (P \lor \neg P)$$. The latter is impossible.