Over at Terence Tao's blog, the Fields medalist produces prodigious volumes of posts; some detail his major research work, some are course lecture notes, and then some are expository bits that he writes up for his own edification. I just noticed a post from April about Gödel's completeness and compactness theorems. From a logician's point of view, the post's contents are by and large pretty vanilla. But early in the post, Tao mentions a notion of elementary convergence and proves the following:

Sequential compactness theorem: Let be a countable language, and let be a sequence of -structures. Then there is a subsequence which elementarily converges to a limit -structure (with a countable universe).

The sequence elementarily converges to if, for any sentence of , implies that for sufficiently large . This notion and the stated result struck me as unfamiliar, but I figured maybe it was just me. However, model theorist John Goodrick also indicated that he'd never come across this notion of elementary convergence either.

Tao gives a quick proof of the theorem as a corollary to compactness, which goes roughly as follows:

Proof. The set of all theories in can of course be identified with where is the (countable) set of sentences from . Moreover, the space with the product topology is sequentially compact because it is a countable product of the sequentially compact . (See Proposition 9 here for instance.) So the sequence of theories in has a subsequence converging to some theory . Using the compactness theorem, it follows that is in fact a consistent theory, and we get a countable model . Without too much ado, one can verify that is indeed an elementary limit of the subsequence.

Note that the restriction on 's countability is essential for this proof to go through, as an uncountable product of sequentially compact spaces need not be sequentially compact. Consider, say, . For let be the -th digit of 's binary expansion, and let be the function . One can check that the sequence has no convergent subsequence.

One reason this formulation might not have gotten much play in model theory itself is that ultraproducts already give us elementary limits of sequences of structures, via Łoś' theorem. Tao's interest in elementary limits arises from his combinatorial pursuits. From his post:

The sequential compactness theorem also lets us construct infinitary limits of various sequences of finitary objects; for instance, one can construct infinite pseudo-finite fields as the elementary limits of sequences of finite fields. I recently discovered that other several [sic] correspondence principles between finitary and infinitary objects, such as the Furstenberg correspondence principle between sets of integers and dynamical systems, or the more recent correspondence principles concerning graph limits, can be viewed as special cases of the sequential compactness theorem;

Let's consider an example of the kind of correspondence principle that Tao has in mind, one which was discussed in detail in an earlier post from Tao's blog. First we have what is essentially a quantitative version of the statement that bounded, monotone sequences of real numbers converge:

Infinite Convergence Principle: For any and any , there exists an such that for all .

Tao goes through some machinations in order to finally arrive at a finitary version of the same principle, which he proves to be quickly interderivable with the infinitary version:

Finite Convergence Principle: If and , and with sufficiently large, then there is an such that for all .

As pointed out by Henry Towsner and Ulrich Kohlenbach in the comments on the post, the finite convergence principle is nothing more than the no-counterexample interpretation of the infinite convergence principle. (See this paper by Kohlenbach and Gaspar for more details.) There has been much recent work applying proof theory to the fields of analysis, combinatorics and ergodic theory. Kreisel's no-counterexample interpretation comes up, for instance, in the formulation of a constructive mean ergodic theorem in the paper "Local stability of ergodic averages" by Avigad, Gerhardy and Towsner. Kohlenbach has a multitude of papers in this area, as well as the monograph Applied Proof Theory: Proof Interpretations and their Use in Mathematics.

We saw above that Tao indicated that the sequential compactness theorem subsumes things like this correspondence between the infinite and finite convergence principles (which is just an instance of the no-counterexample interpretation, or at its heart, Herbrand's theorem) and correspondence principles concerning graph limits à la Elek and Szegedy (who use an ultraproduct construction). So it distills a common logical thread that runs through these results. I might write another post about the logical status of this sequential compactness theorem later. (Then again, I might very well not.)