Compactness via Tychonoff? I was reminded just now of something I wondered about  years ago:
It's well known that one can derive the compactness theorem in propositional logic from the Tychonoff theorem. What about FOL?
I think I actually made some progress on this just now. The following lemma is clear just on general set-theoretic grounds:


Lemma. If every finite subset of $\sum$ has  model then there exists a cardinal $\kappa$ such that every finite subset of $\sum$ has a model of cardinality less than $\kappa$.


And it seems to me a Tychonoffian proof of compactness may be straightforward from that. (Say $X$ is the  ordinal $\kappa +1$. Then the set of all structures with "universe" $X$ is(?) compact in a big product topology, hence qed. If necessary we could compactify the set of all structures with universe a subset of $X$ by adding a function $U:X\to\{0,1\}$ and regarding the  universe as $\{x\in X:U(x)=1\}$.)
Q: Does that work?
(I suppose if I ask for "proof-verification" I should at least give the proof I have in mind. Sorry - it would be arbitrarily tedious to write  down a sketch of all the details. If as I  suspect the answer is yes then I suspect it will be clear to  anyone likely to  know the answer what proof  I have in mind. Heh, before hitting the "not clear what you're asking" button please ask someone like Noah or Asaf whether it's clear to them...)
 A: As far as I know, there is no way to use Tychonoff to prove the compactness of first-order logic.
First, note that the lemma can be improved drastically: by the Lowenheim-Skolem theorem, we can take $\kappa=\aleph_0$. So that makes things a bit more concrete. It will also be convenient to assume (WLOG) that our set of sentences whose satisfiability we're trying to prove contains the sentence "There are at least $n$ distinct elements" for every finite $n$, so we only have to care about infinite structures.
Putting the above together, we now want to consider a "space of structures" with domain $\mathbb{N}$. And here we run into a problem: what's our topology?
In the propositional case, the topology on the set of truth assignments was generated by the "simple facts" - the basic opens were the cylinders $\{\nu: \nu(p)=1\}$ and $\{\nu: \nu(p)=0\}$ for $p$ a propositional variable. The analogous topology here is that generated by atomic and negated atomic sentences in our language together with natural numbers (= elements of the domain of our structure) as parameters, and it's not hard to show that that's compact.
But now things get ugly. In the propositional case, all propositional sentences were generated from the atoms via finite Boolean combinations, hence corresponded to open sets in this "simple" topology. In the first-order case, that's not true anymore: e.g. if we have a unary predicate $U$, the sentence $\forall x(U(x))$ does not correspond to an open set. The quantifier-free fragment of first-order logic does indeed closely resemble propositional logic, and the corresponding topology on structures is indeed easily seen to be compact, but full first-order logic is much more complicated and requires a more complicated topology: the topology we actually care about for the purposes of the compactness of first-order logic is generated by all first-order sentences - that is, the basic open sets are those of the form $\{M: M\models\varphi\}$ for $M$ a structure in our language with domain $\mathbb{N}$ and $\varphi$ a sentence in our language together with natural number parameters.

Roughly speaking, I'd say that the message is this. In all our semantic contexts, "structures" are determined by their "finite approximations." But the nature of this determination is not always the same. In "weak" logics like propositional logic, every fact is determined by some individual finite approximation (= "every propositional sentence can only use finitely many propositional atoms"), but in "strong" logics like first-order logic we need to look at all the finite approximations at once to tell what's going on. As soon as the latter situation happens, the relevant topology is no longer a product topology coming from finite approximations, and hence Tychonoff no longer gives us compactness.
