Tychonoff theorem in the finite case and choice Is it possible to prove the Tychonoff theorem in the finite case (the product of a finite number of compact spaces is compact), without using the axiom of choice ?
My guess is yes but the proofs I've seen seem to use a form of choice at some point. (By choosing for all points of a space a given open set containing it...) 
 A: It suffices to prove that the product of two compact spaces is compact. Let $X$ and $Y$ be compact; $X\times Y$ is compact if and only if every filter on $X\times Y$ has a cluster point, so let $\mathscr{F}$ be a filter on $X\times Y$. Let $\pi_X:X\times Y\to X$ and $\pi_Y:X\times Y\to Y$ be the canonical projection maps.
Let 
$$\mathscr{G}_X=\{G\subseteq X:\pi_X^{-1}[G]\in\mathscr{F}\}\;;$$
$\mathscr{G}_X$ is a filter on $X$, so it has a cluster point $p$. Let $\mathscr{F}'$ be the filter on $X\times Y$ generated by
$$\mathscr{F}\cup\{\pi_X^{-1}[U]:U\text{ is a nbhd of }p\}\;,$$
let
$$\mathscr{G}_Y=\{G\subseteq Y:\pi_Y^{-1}[G]\in\mathscr{F}'\}\;,$$
a filter on $Y$, and let $q$ be a cluster point of $\mathscr{G}_Y$. Let $\mathscr{F}''$ be the filter on $X\times Y$ generated by
$$\mathscr{F}'\cup\{\pi_Y^{-1}[U]:U\text{ is a nbhd of }q\}\;.$$
Then $\langle p,q\rangle$ is a cluster point of $\mathscr{F}$.
To see this, let $U$ be any open nbhd of $\langle p,q\rangle$ in $X\times Y$. There are open nbhds $V$ of $p$ and $W$ of $q$ such that $\langle p,q\rangle\in V\times W\subseteq U$, and by construction $\pi_X^{-1}[V]\in\mathscr{F}'\subseteq\mathscr{F}''$. And $\pi_Y^{-1}[W]\in\mathscr{F}''$, so
$$V\times W=\pi_X^{-1}[V]\cap\pi_Y^{-1}[W]\in\mathscr{F}''\;.$$
Thus, $U\in\mathscr{F}''$, so $U\cap F\ne\varnothing$ for each $F\in\mathscr{F}$, and $\langle p,q\rangle$ is a cluster point of $\mathscr{F}$.
There is no use of $\mathsf{AC}$ here: the argument requires just three choices, of $p$, $q$, and the pair $\langle V,W\rangle$.
A: Yes this is possible. Let $O$ be an open cover of $X\times Y$.
Since the topology is generated by sets of the form $U\times V$ we can replace $O$ by $$O_1=\{U\times V|\exists W\in O, U\times V\subseteq W\}$$
It suffices to show that $O_1$ has an open cover.
Define an open cover of $X$ as follows: an open set $U\subseteq X$ is in the cover if there is a finite collection $\{V_i\}$ of open subseteq of $Y$ such that
1)$U\times V_i\in O_1$
2) $U\times Y \subseteq \bigcup U\times V_i$.
This is an open cover for if $x\in X$ take $U_i\times V_i$ finite covering $\{x\}\times Y$. Then $\cap U_i$ is in our cover and $x\in \cap U_i$.
Let $F$ be a finite subcover of this covering for $X$. Then for each $U\in F$, find finite $V_i$ such that $U\times Y \subseteq \cup U\times V_i$.
Now we are done.
