Tychonoff's Theorem via the Compactness Theorem for propositional logic I am trying to prove Thychonoff's Theorem using the Compactness Theorem for propositional logic.
A space $X$ is compact if and only if every collection $C$ of closed subsets of $X$ having the finite intersection property has nonempty intersection.
Hence, I am trying to show that given a family of compact spaces $\{X_{i}\}_{i\in I}$ then their product $X=\prod_{i\in I}X_{i}$ is compact by showing that an arbitrary family $C$ of closed subsets of $X$ having the f.i.p. has non-empty intersection.
I run into trouble defining the appropriate set $S$ of propositional formulas. And, in fact it seems we may need the $X_{i}$ to be also Hausdorff, since once $S$ is shown to be satisfiable it seems reasonable to use any assignment satisfying $S$ in order to define a non-empty set (perhaps a single point) which will be contained in $\cap C$ and thus show that the intersection is non-empty.
May someone point me in the right direction? Or perhaps there is a more direct argument not relying on the f.i.p. formulation of compactness?
Disclaimer: I have not learned first order logic yet. Hence, this related question does not really answer mine, as far as I can tell.
 A: Let $\{X_i\}_{i\in I}$ be a family of compact spaces, and let $X = \prod_{i\in I} X_i$. Let $C$ be a family of closed subsets of $X$ with the f.i.p.
Notation: For $Y_i\subseteq X_i$, let's write $\tilde{Y_i}$ for the set $Y_i\times \prod_{j\neq i} X_i\subseteq X$. The sets $\tilde{U_i}$ with $U_i$ open in $X_i$ form a subbasis for the topology on $X$, so a basic open set has the form $\tilde{U}_{i_1}\cap \dots \cap \tilde{U}_{i_n}$, where each $U_{i_j}$ is open in $X_{i_j}$. Then a basic closed set has the form $\tilde{V}_{i_1}\cup \dots \cup \tilde{V}_{i_n}$.
Let's begin with the standard observation that we can replace $C$ with a family of basic closed sets. Indeed, every closed set is the intersection of all the basic closed sets containing it, so letting $$C' = \{V'\mid V'\text{ basic closed, and }V\subseteq V'\text{ for some }V\in C\}$$
we have $\bigcap_{V\in C} V = \bigcap_{V'\in C'} V'$ and $C'$ also has the f.i.p. So we can assume every closed set in $C$ is a basic closed set.
For every closed set $F\subseteq X_i$, introduce a proposition symbol $P_F^i$. A point of $X$ can be written as $(x_i)_{i\in I}$, and we think of $P_F^i$ as meaning "$x_i\in F$".
Now consider the following propositional theory $T$:

*

*For all $V\in C$, with $V = \tilde{V}_{i_1}\cup \dots \cup \tilde{V}_{i_n}$, $T$ contains the axiom $$P^{i_1}_{V_{i_1}}\lor \dots \lor P^{i_n}_{V_{i_n}}.$$

*For all $i\in I$ and all closed sets $F_1,\dots,F_n$ in $X_i$, if $\bigcap_{j=1}^{n}F_j = \varnothing$, then $T$ contains the axiom $$\lnot \bigwedge_{j=1}^{n} P^i_{F_j}.$$

*For all $i\in I$ and all closed sets $F,F'$ in $X_i$, if $F\cup F'= X_i$, then $T$ contains the axiom $$P^i_{F}\lor P^i_{F'}.$$
I claim that $T$ is consistent. By compactness, it suffices to show that we can find an assignment satisfying all axioms from schemas 2 and 3, together with finitely many axioms from schema 1, corresponding to finitely many $V_1,\dots,V_m\in C$. By the hypothesis that $C$ has f.i.p., we can pick some $x = (x_i)_{i\in I}\in V_1\cap\dots\cap V_m$. For each proposition symbol $P^i_F$, set $P^i_F$ to be true if $x_i\in F$ and false otherwise. It is straightforward to check that this assignment works.
Since $T$ is consistent, there is some assignment $t$ from our proposition symbols to $\{\top,\bot\}$ satisfying $T$.
Fix $i\in I$. I claim that $C_i = \{F\subseteq X_i\mid F\text{ closed, and }t(P^i_F) = \top\}$ has non-empty intersection. Since $X_i$ is compact, it suffices to show that $C_i$ has the f.i.p. Let $F_1,\dots,F_n\in C_i$. If $\bigcap_{j=1}^n F_j = \varnothing$, then the axiom $\lnot\bigwedge_{j=1}^n P^i_{F_j}$ is in $T$, so we cannot have $t(P^i_{F_j}) = \top$ for all $1\leq j\leq n$, contradiction.
Thus we can pick $x_i\in \bigcap_{F\in C_i}F$ for all $i\in I$. I claim that $x = (x_i)_{i\in I}\in\bigcap_{V\in C} V$. For each $V\in C$ with $V = \tilde{V}_{i_1}\cup \dots \cup \tilde{V}_{i_n}$, $T$ contains the axiom $P^{i_1}_{V_{i_1}}\lor \dots \lor P^{i_n}_{V_{i_n}}$. So for some $1\leq j\leq n$, $t(P^{i_j}_{V_{i_j}}) = \top$. Then $V_{i_j}\in C_{i_j}$, so $x_{i_j}\in V_{i_j}$, so $x\in V$.

Great! But note that above, we have to use the axiom of choice to pick $x_i\in \bigcap_{F\in C_i}F$ for all $i\in I$. If you want to prove Tychonoff's Theorem from compactness for propositional logic relative to ZF, then you need to additionally assume that each $X_i$ is Hausdorff.
The fix is that when $X_i$ is compact Hausdorff, the set $\bigcap_{F\in C_i}F$ is a singleton $\{x_i\}$, so there is no choice to be made. Suppose $x,y\in \bigcap_{F\in C_i}F$ with $x\neq y$. Since $X_i$ is Hausdorff, we can find disjoint open neighborhoods $U_x$ and $U_y$ of $x$ and $y$, respectively. Let $F_x = X_i\setminus U_x$, and let $F_y = X_i\setminus U_y$. Since $x\notin F_x$, we must have $t(P^i_{F_x}) = \bot$. And since $y\notin F_y$, we must have $t(P^i_{F_y}) = \bot$. But since $U_x\cap U_y = \varnothing$, $F_x\cup F_y = X_i$, so the axiom $P^i_{F_x}\lor P^i_{F_y}$ is in $T$. This is a contradiction.
Note that we only used axiom schema 3 in the choiceless proof for compact Hausdorff spaces. But it didn't hurt to throw these axioms into $T$ in the proof for compact spaces as well.
