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.

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. 


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):
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.) 


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. 


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. 


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. 


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......... 


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. 

