Why is compactness in logic called compactness?

In logic, a semantics is said to be compact iff if every finite subset of a set of sentences has a model, then so to does the entire set.

Most logic texts either don't explain the terminology, or allude to the topological property of compactness. I see an analogy as, given a topological space X and a subset of it S, S is compact iff for every open cover of S, there is a finite subcover of S. But, it doesn't seem strong enough to justify the terminology.

Is there more to the choice of the terminology in logic than this analogy?

The Compactness Theorem is equivalent to the compactness of the Stone space of the Lindenbaum–Tarski algebra of the first-order language $L$. (This is also the space of $0$-types over the empty theory.)

A point in the Stone space $S_L$ is a complete theory $T$ in the language $L$. That is, $T$ is a set of sentences of $L$ which is closed under logical deduction and contains exactly one of $\sigma$ or $\lnot\sigma$ for every sentence $\sigma$ of the language. The topology on the set of types has for basis the open sets $U(\sigma) = \{T:\sigma\in T\}$ for every sentence $\sigma$ of $L$. Note that these are all clopen sets since $U(\lnot\sigma)$ is complementary to $U(\sigma)$.

To see how the Compactness Theorem implies the compactness of $S_L$, suppose the basic open sets $U(\sigma_i)$, $i\in I$, form a cover of $S_L$. This means that every complete theory $T$ contains at least one of the sentences $\sigma_i$. I claim that this cover has a finite subcover. If not, then the set $\{\lnot\sigma_i:i\in I\}$ is finitely consistent. By the Compactness Theorem, the set consistent and hence (by Zorn's Lemma) is contained in a maximally consistent set $T$. This theory $T$ is a point of the Stone space which is not contained in any $U(\sigma_i)$, which contradicts our hypothesis that the $U(\sigma_i)$, $i\in I$, form a cover of the space.

To see how the compactness of $S_L$ implies the Compactness Theorem, suppose that $\{\sigma_i:i\in I\}$ is an inconsistent set of sentences in $L$. Then $U(\lnot\sigma_i),i\in I$ forms a cover of $S_L$. This cover has a finite subcover, which corresponds to a finite inconsistent subset of $\{\sigma_i:i\in I\}$. Therefore, every inconsistent set has a finite inconsistent subset, which is the contrapositive of the Compactness Theorem.

The analogy for the compactness theorem for propositional calculus is as follows. Let $p_i $ be propositional variables; together, they take values in the product space $2^{\mathbb{N}}$. Suppose we have a collection of statements $S_t$ in these boolean variables such that every finite subset is satisfiable. Then I claim that we can prove that they are all simultaneously satisfiable by using a compactness argument.

Let $F$ be a finite set. Then the set of all truth assignments (this is a subset of $2^{\mathbb{N}}$) which satisfy $S_t$ for $t \in F$ is a closed set $V_F$ of assignments satisfying the sentences in $F$. The intersection of any finitely many of the $V_F$ is nonempty, so by the finite intersection property, the intersection of all of them is nonempty (since the product space is compact), whence any truth in this intersection satisfies all the statements.

I don't know how this works in predicate logic.

Lemma: A topological space $X$ is compact if and only if for every collection $\mathcal{C}$ of closed sets with the finite intersection property has nonempty intersection over the collection.

Proposition: $\mathbb{M}(\mathcal{L})$ is compact if and only if every finitely satisfiable $\mathcal{L}$-theory is satisfiable.

Proof: Consider the space $\mathbb{M}(\mathcal{L})=\{\Phi \; | \; \Phi \; \text{is a maximal} \; \mathcal{L} \text{-theory}\}$. For each $\mathcal{L}$-sentence $\varphi$ let $[(\varphi)]=\{ \Phi \in \mathbb{M}(\mathcal{L}) \; | \; \varphi \in \Phi\}$. A subbase $\cal{B}$ for a topology on $\mathbb{M}(\mathcal{L})$ is given by the sets $[(\varphi)]$. That is, the open subsets of $\mathbb{M}(\mathcal{L})$ are the union of the finite intersections of elements of $\mathcal{B}$. To see that $\mathcal{B}$ defines a topology on note that $[(\forall x(x\neq x))]=\emptyset$ and $[(\forall x(x=x))]=\mathbb{M}(\mathcal{L})$. Furthermore, arbitrary unions are already defined to be in the topology and finite intersections are in the topology since $[(\varphi)]\cap [(\theta)]=[(\varphi \wedge \theta)]$, which is defined to be open.

Assume logical compactness. Note that $\bigcap_{i\in I} [(\varphi_i)]=\emptyset$ if and only if it is not satisfiable. Let $\mathcal{C}$ be a subcollection of the subbasis of the topology of $\mathbb{M}(\mathcal{L})$ with the finite intersection property. Then every finite subset of $\mathcal{C}$ is satisfiable and by the compactness theorem this implies $\bigcap [(\varphi)]$ which ranges over all the elements of $\cal{C}$ is satisfiable, hence $$ \bigcap_{[(\varphi)] \in \cal{B}} [(\varphi)]\neq \emptyset. $$ Thus $\mathbb{M}(\mathcal{L})$ is compact.

Assume $\mathbb{M}(\mathcal{L})$ is compact. Let $\Phi$ be an $\mathcal{L}$-theory in which is finitely satisfiable. Let $\mathcal{C}_\Phi=\{[(\varphi)] \; | \; \varphi \in \Phi\}$. Every element of $\mathcal{C}_\Phi$ is closed and every finite subset of $\mathcal{C}_\Phi$ has nonempty intersection since $\Phi$ is finitely satisfiable. Since $\mathbb{M}(\mathcal{L})$ is compact, $\bigcap_{\varphi \in \Phi} [(\varphi)]\neq\emptyset$, hence it is satisfiable. $\square$

A motto which is related (and sometimes true) is "proofs are finite". In most systems of logic under consideration, the statement and a proof of the statement are finite strings of symbols. One can think of them as "compactly" represented. How nice then that certain systems will always allow a proof to be found if there is one. While this does not give a tight connection to topology, it suggests (and you need to work this through on your own to be convinced) that certain infinite abnormalities (like an infinite proof) will not occur. A similar topological claim is that, for compact sets, an infinite inclusive chain of certain subsets will have nonempty intersection, such a claim easily seen to be false for some non-compact sets, such as the collection { C_n | C_n = {x | x >= n and x is a real number } for n a non-negative integer } .