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.
Best Answer
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.
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.
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.