Proving Tychonoff's theorem with the Compactness theorem of logic It seems to be known that Tychonoff's Theorem for Hausdorff spaces and the Compactness theorem of first order logic are both equivalent over ZF to the ultrafilter lemma. Does anyone know a slick proof for the implication "Compactness Theorem $\rightarrow$ Tychonoff for Hausdorff spaces" (without using the ultrafilter lemma as an intermediate step)?
 A: Suppose that we have a family of compact Hausdorff space $(X_i, \tau_i)$ where $\tau_i$ is the topology and $i$ ranges over an index set $I$. Assume that the product $X = \prod_i X_i$ is not compact, so there is an open cover $(W_\alpha: \alpha < \kappa)$ of $X$ which does not have a finite subcover. We define a language and a consistent theory and then apply the compactness theorem to get a point in $X - \bigcup_\alpha W_\alpha$.
W.l.o.g, assume that each $W_\alpha = \prod_i W_{\alpha,i}$ for $W_{\alpha,i} \in \tau_i$ and $spt(W_\alpha) = \{i: W_{\alpha,i} \neq X_i\}$ is finite. 
The language consists of


*

*constants $c_i$ for $i \in I$;

*for each $i$ and each $U \in \tau_i$, a unary predicate $P_{i,U}$.


The intended meaning of $(c_i: i \in I)$ is a (non-standard) point in $X - \bigcup_\alpha W_\alpha$; and $P_{i,U}(x)$ means $x \in U$.
The theory $T$ consists of


*

*$P_{i,X_i}(c_i)$;

*for each $\alpha$, $\bigvee_{i \in spt(W_\alpha)} \neg P_{i,W_{\alpha,i}}(c_i)$ (i.e., $(c_i: i \in I) \not\in W_\alpha$);

*for each finite $F \subset \tau_i$, if $\bigcup_{U \in F} U = X_i$ then the sentence $(\forall x) (P_{i,X_i}(x) \to \bigvee_{U \in F} P_{i,U}(x))$ is in $T$;

*if $C = X_i - U$ is closed and $U_0, U_1 \in \tau_i$ are s.t. $U_i \cap C \neq \emptyset$ and $U_0 \cap U_1 \cap C = \emptyset$, then the sentence $\neg P_{i,U_0}(c_i) \vee \neg P_{i,U_1}(c_i)$ is in $T$.


By the assumption that $W_\alpha$'s do not have a finite subcover, $T$ is consistent. So take a model $M$ of $T$, let $\mathcal{C}_i$ be the set of $X_i - U$ s.t. $U \in \tau_i$ and $M \models \neg P_{i,U}(c_i)$. Then $\mathcal{C}_i$ has finite intersection property and by compactness $\bigcap \mathcal{C}_i$ is non-empty. By the last set of sentences in $T$, $\bigcap \mathcal{C}_i$ is a singleton $\{p_i\}$ (here we need Hausdorff-ness). The point $(p_i: i \in I)$ is not covered by any $W_\alpha$.
