I have a somewhat vague question. It seems to me that there are two main ways in which ultrafilters (on a set) can be used. One is in topology. The notion of an ultrafilter converging to a point is very useful since, in particular, knowing the limit points of every ultrafilter on a space is equivalent to knowing its topology. The other use is in logic (a subject about which I admittedly know very little). For instance, ultraproducts (and more generally ultralimits) can be used to construct nonstandard models etc. I'm just curious about any connections that exist between these two uses of ultrafilters. For example, is there any logical interpretation of ultrafilter convergence on a topological space, etc? Is there a connection to the internal logic of its topos of sheaves for example? I'm really a beginner with this stuff, so any interesting connections, even trivial ones, would be most interesting to me. If this question is too openended, feel free to change this to community wiki.

1$\begingroup$ Ultrafilters are also used in forcing in set theory, with the same effect as in the construction of ultraproducts, namely a quotient by an ultrafilter collapses a complete Boolean algebra to the Boolean algebra $\lbrace 0,1 \rbrace$. $\endgroup$ – Andrej Bauer May 27 '10 at 10:38

1$\begingroup$ Here are two very good pieces of exposition on ultrafilters: topologicalmusings.wordpress.com/2008/07/18/… and terrytao.wordpress.com/2007/06/25/… $\endgroup$ – David Corfield May 27 '10 at 12:40

$\begingroup$ This is very closely related to this question  mathoverflow.net/questions/11261/… $\endgroup$ – François G. Dorais♦ May 27 '10 at 17:56

$\begingroup$ Thanks very much for all the answers! I'm avoiding accepting an answer as the question can clearly have multitude of "correct" answers. $\endgroup$ – David Carchedi Jun 1 '10 at 13:11
Some of the connections between topology and logic via ultrafilters have been around for quite a while.
Łoś's theorem from 1955 is the first place where ultraproducts appear in logic, as far as I know, although the ultraproduct construction is older (probably due to Hewitt). A very elegant proof of the compactness theorem of firstorder logic using ultraproducts is due to Morel, Scott, and Tarski. It shows that compactness in logic is really compactness of an appropriate topological space. This pretty and inspiring connection can be extended much further.
A very nice starting point to learn about these connections is the series of papers by Xavier Caicedo (no relation):
 Compactness and normality in abstract logics. Ann. Pure Appl. Logic 59 (1993), no. 1, 3343.
 The abstract compactness theorem revisited. Logic and foundations of mathematics (Florence, 1995), 131141, Synthese Lib., 280, Kluwer Acad. Publ., Dordrecht, 1999.
 Logic of sheaves of structures. (in Spanish) Rev. Acad. Colombiana Cienc. Exact. Fís. Natur. 19 (1995), no. 74, 569586.
The last paper shows how many "limit" constructions in intuitionistic logic (Kripke models), set theory (forcing) and elsewhere are examples of the same phenomenon.
This topological approach to logic is mainly guided by the ultraproduct construction. Daniele Mundici has also written about this.
Paolo Lipparini has studied variants of compactness that also turn out to have connections to logic via properties of ultrafilters, and lead to very interesting problems that seem to require Shelah's pcf theory; this line of work seems to have originated in settheoretic topology, and R. Stephenson wrote a good survey (25 years old now) of the then state of the art as far as the topological side of things, see his article in the Handbook of SetTheoretic Topology.
Finally, set theory is nowadays where both ultrafilters in general and the ultraproduct construction in particular are mostly used, in connection with large cardinals and elementary embeddings. Many natural problems in settheoretic topology have been shown to have deep connections with these cardinals via the ultrafilters they generate. (Though here the connection to logic proper is weaker.)
Another interesting use of ultrafilters takes place in metric geometry, where they are used for constructing the socalled asymptotic cones of metric spaces.
Roughly speaking, an asymptotic cone of a metric space $X$ is what you see when looking at $X$ from infinitely far away. More precisely, you rescale the metric on $X$ dividing by $n$, you let $n$ tend to $+\infty$, and you take the GromovHausdorff limit point of the obtained sequence of metric spaces. Of course, usually such a sequence does not converge, and you use a nonprincipal ultrafilter for individuating a limit (depending on the ultrafilter). The idea is due to Gromov and has been first described in detail by van den Dries and Wilkie in:
Gromov's theorem on groups of polynomial growth and elementary logic. J. Algebra 89 (1984), no. 2, 349374.
Another way of constructing asymptotic cones is as follows: you take a nonstandard extension $^\ast X$ of $X$ with nonstandard distance $^\ast d$ induced by the distance $d$ on $X$, you choose an infinite nonstandard real $\lambda$ and you identify points $p,q$ of $^\ast X$ if $^\ast d (p,q)/\lambda$ is infinitesimal. You put on the quotient the metric $d'=^\ast d/\lambda$, thus obtaining an asymptotic cone of $X$ (I am cheating a bit: you should also choose a basepoint in $^\ast X$ and consider only points in the quotient of $^\ast X$ which are at finite $d'$distance from the basepoint).
Asymptotic cones are nowadays a useful tool in geometric group theory, where they are used for studying largescale properties of groups and spaces.

$\begingroup$ A beautiful reply, thank you for this! $\endgroup$ – Grant Olney Passmore May 28 '10 at 0:03
It's a multifaceted question, and answers will be multifaceted too.
At a simpler level, you know doubt know that an ultrafilter on a set $X$ can be identified with a Boolean algebra homomorphism $PX \to P1$. More generally, an ultrafilter in a Boolean algebra $B$ is a Boolean algebra homomorphism $B \to P1$, and if we think of $B$ (or a presentation of $B$) as a propositional theory, then such Boolean algebra homomorphisms or truthvalue assignments to propositions $b \in B$ can be thought of as models for the theory. The set of all Boolean algebra homomorphisms can be topologized a la Zariski, and the result is a Stone space (cf. supercooldave's reply) which is compact, Hausdorff, and totally disconnected. The compactness in particular directly implies the compactness theorem for propositional theories: thinking of propositions $b \in B$ as giving closed sets in the Zariski spectrum, if every finite conjunction of propositions from a set $\Sigma$ has a model (or a point in the Stone space), then $\Sigma$ itself has a model (i.e., the intersection of all closed sets coming from $b \in \Sigma$ is nonempty). This principle can be beefed up to encompass the compactness theorem for predicate logic.
Here's another crossconnection (since you bring up nonstandard models): the ultrapowers or ultraproducts, used to construct for example Robinson's nonstandard reals, are just examples of taking stalks. That is: if you have a bunch of models $M_x$ indexed by a set $X$, and if you have an ultrafilter on $X$ (realized as a point $U$ in the StoneCech compactification $\beta X$ of the discrete space $X$), then the ultraproduct
$$(\prod_{x \in X} M_x)/U$$
is the value of the structure $(M_x)_{x \in X}$ (as an object in the topos $Set/X$) under the composite functor
$$Set/X \simeq Sheaves(X_{discrete}) \stackrel{i_*}{\to} Sheaves(\beta X) \stackrel{stalk_U}{\to} Set$$
where $i_*$ is a geometric morphism between sheaves induced by the canonical continuous inclusion of $X$ into $\beta X$. Lawvere has remarked that both Robinson's construction and Cohen forcing are examples of a general phenomenon, where one starts with a model in a universe $Set$ of presumably constant sets, then passes to a universe of more variable sets (such as $Set/X$, $Sh(\beta X)$, or $Sh(P)$ where $P$ can be a poset of "forcing conditions"), and then passes back down again to more constant sets by "freezing at a point" (taking stalks at a point, or passing to a filterquotient construction)  even if mention of the passage through toposes of variable sets is usually elided over in silence.

$\begingroup$ Wow, that's really cool! Thanks! Is there anywhere I can read more about this? $\endgroup$ – David Carchedi May 27 '10 at 13:10

1$\begingroup$ Mac Lane and Moerdijk's book "Sheaves in Geometry and Logic" spells out the connections very nicely. $\endgroup$ – Steven Gubkin May 27 '10 at 13:23

$\begingroup$ I'm going on memory here, but I may have picked up on the ideas in the first paragraph by reading the first few chapters of Handbook of Mathematical Logic. Johnstone's book is also really good, and goes into a lot of detail. We're adding bits and pieces to the nLab (e.g., stuff surrounding "ultrafilter theorem"). As for the stuff in the last paragraph, you probably have Mac LaneMoerdijk as a reference; the stuff from Lawvere comes from his Chicago lecture notes Variable Sets, Etendu, and Variable Structures in Topoi. Sorry I don't have more! $\endgroup$ – Todd Trimble♦ May 27 '10 at 13:30

$\begingroup$ Todd, you might want to check out this old question of Joel David Hamkins  mathoverflow.net/questions/11261/…  My answer there overlaps with yours, but you probably could add your two cents. $\endgroup$ – François G. Dorais♦ May 27 '10 at 17:55

$\begingroup$ Thanks for bringing this to my attention, Francois. I may have something to add a little later. $\endgroup$ – Todd Trimble♦ May 27 '10 at 18:18
Speaking of asymptotic cones ... here's another connection between ultrafilters, topology and logic. Suppose that $\Gamma$ is a uniform lattice in $SL_{3}(\mathbb{R})$. Gromov suggested that the asymptotic cones of $\Gamma$ are ``(essentially) independent of the choice of the ultrafilter $\mathcal{D}$.'' In fact, the following is true:
(a) If $CH$ holds, then $\Gamma$ has a unique asymptotic cone up to homeomorphism.
(b) If $CH$ fails, then $\Gamma$ has $2^{2^{\omega}}$ asymptotic cones up to homeomorphism.
Amongst other things, the proof involves some ideas from nonstandard analysis. The relevant reference is:
L. Kramer, S. Shelah, K. Tent and S. Thomas Asymptotic cones of finitely presented groups, Advances in Mathematics 193 (2005), 142173.

$\begingroup$ CH is continuum hypothesis? Wow, that's quite a remarkable result. $\endgroup$ – David Carchedi May 27 '10 at 21:27

$\begingroup$ Yes, $CH$ is the continuum hypothesis. The corresponding result is probably also true of the nonuniform lattice $SL_{3}(\mathbb{Z})$ ... but this question has been open for some years now. $\endgroup$ – Simon Thomas May 27 '10 at 21:29
My feeling, which may be ignorant, is that these intuitions go all the way back to Leibniz. There "point" was in some way ridded of a silly definition like "position but no magnitude", and was replaced by a "sequence of more and more accurate propositions". What "proposition" means to logicians has moved on since then (Frege). But Leibniz's "principle of indiscernibles" states that if A and B are different, then something is true of A and not of B. An early separation axiom. His pointlike things became objects of metaphysics, but no one's perfect.
If model theory worked more explicitly with a "space of models", which no doubt for good reasons it doesn't, the analogy would be clearer to everyone. For the logical reading of sheaf theory and topos theory, the way of equating open sets with propositions is rather fundamental, though tacit.

$\begingroup$ You've stated the indiscernibility of identicals (contrapositive). $(F)x=y\supset (Fx\equiv Fy)$ I believe Leibniz's law is the identity of indiscernables. $(F)(Fx\equiv Fy)\supset x=y$ Very interesting point about separation. $\endgroup$ – Jeremy Shipley Jun 6 '10 at 16:09

$\begingroup$ I see that I messed up that first formula. The quantifier should be in consequent of course. $\endgroup$ – Jeremy Shipley Jun 6 '10 at 18:48
There is a rising use of ultrafilters in number theory,particularly additive number theory,as topological tools are being used to either simplify previous results or to develop new ones. Melvyn Nathanson recently gave a pair of asyetunpublished lectures describing Glazer's use of ultrafilters in giving a vastly simplified proof of Hindman's theorem. I plan to pursue this line of research this summer and I hope to make it the basis of my first published results by fall.Stay tuned.........

$\begingroup$ Andrew, since I think you are in New York City, drop me an email if you'd like to meet up and discuss ultraproducts. $\endgroup$ – Joel David Hamkins May 28 '10 at 2:30

$\begingroup$ I certainly am,Joeland if you're at the City University of New York Graduate Center,I'd love to meet you for coffee to talk about it later this summer! $\endgroup$ – The Mathemagician May 28 '10 at 3:49

$\begingroup$ Lots about that is available in the monograph of Hindman and Strauss, Algebra in the StoneCzech Compactification. I am writing a course on this stuff, the beginning of which (including the GalvinGlazer proof) already availabe. $\endgroup$ – Boaz Tsaban May 2 '14 at 15:41
The book Stone Spaces by Peter T. Johnstone could be one place to begin your search. It investigates deeply one connection between topology and logic. Topology via Logic by Steven Vickers covers similar territory. (I could say more, but both books are in my home library.)
Ultrafilters appear naturally as ultraproducts in the space of marked groups as introduced by V. Guirardel and C. Champetier in Limit groups as limits of free groups. Indeed, if $(G_k,\phi_k)$ is a sequence of marked groups converging to some marked group $(G,\phi)$, then, for every nonprincipal ultrafilter $\omega$ on $\mathbb{N}$, $G$ embeds into the ultraproduct $\prod\limits_{n \in \mathbb{N}} G_k / \omega$. This key observation links convergence in the space of marked groups and universal theory of groups. For example, it can be proved that limit groups are exactly the finitely generated groups with the same universal theory as a free groups of finite rank, thanks to a embedding into $^{\omega}\mathbb{F}_2$. (See also Nonstandard free groups, written by I. Chiswell, for an approach based on real trees.)
In Structure and rigidity in hyperbolic groups, E. Rips and Z. Sela combined ultralimits of metric spaces and Rips theory to show their shortening argument. For instance, they applied it to show that the automorphism group of a torsionfree hyperbolic group is finitely generated. The shortening argument is also a key result for MakaninRazborov diagrams, and more generally for Sela's solution of Tarski problem.