What are some results in mathematics that have snappy proofs using model theory? I am preparing to teach a short course on "applied model theory" at UGA this summer.  To draw people in, I am looking to create a BIG LIST of results in mathematics that have nice proofs using model theory.  (I do not require that model theory be the first or only proof of the result in question.)
I will begin with some examples of my own (the attribution is for the model-theoretic proof, not the result itself).

*

*An injective regular map from a complex variety to itself is surjective (Ax).


*The projection of a constructible set is constructible (Tarski).


*Solution of Hilbert's 17th problem (Tarski?).


*p-adic fields are "almost C_2" (Ax-Kochen).


*"Almost" every rationally connected variety over Q_p^{unr} has a rational point (Duesler-Knecht).


*Mordell-Lang in positive characteristic (Hrushovski).


*Nonstandard analysis (Robinson).
[But better would be: a particular result in analysis which has a snappy nonstandard proof.]
Added: The course was given in July of 2010.  So far as I am concerned, it went well.  If you are interested, the notes are available at
http://alpha.math.uga.edu/~pete/MATH8900.html
Thanks to everyone who answered the question.  I enjoyed and learned from all of the answers, even though (unsurprisingly) many of them could not be included in this introductory half-course.  I am still interested in hearing about snappy applications of model theory, so further answers are most welcome.
 A: This one https://arxiv.org/abs/0909.2190 is brand new. ".... For a simple linear group G, we show that a finite subset X with |X X-1 X |/ |X| bounded is close to a finite subgroup, or else to a subset of a proper algebraic subgroup of G....". I understand that people in additive combinatorics consider it useful.
A: Hilbert's Seventeenth Problem: Let $f \in \mathbb{R}(x_1, x_2, \ldots, x_n)$ be a rational function which is positive everywhere on $\mathbb{R}^n$. Then there exist rational functions $g_1$, $g_2$, ..., $g_N$ such that $f=\sum g_i^2$. 
Proof sketch: Let $K$ be the field $\mathbb{R}(x_1, x_2, \ldots, x_n)$. If $f$ is not a sum of squares, then there is a total ordering of $K$ where $f$ is negative. Let $L$ be the real closure of $K$ with respect to that ordering. Then the rational function $f$, evaluated at the point $(x_1, x_2, \ldots, x_n) \in L^n$, is negative. But the theory of real closed fields is complete, so $f$ must be negative somewhere in $\mathbb{R}^n$, contrary to hypothesis.
See Jacobson Basic Algebra II for a detailed exposition.
A: You can find lots of other applications just by browsing the titles of the papers on the MODNET preprint server (follow this link and look under "Publications" on the left side of the page).  For example:


*

*"The monomorphism problem in free groups", by L. Ciobanu and A. Ould Houcine (in which they show it is decidable);

*"An invitation to model-theoretic Galois theory," by A. Medvedev and Ramin Takloo-Bighash -- expository paper explaining how the Galois correspondence can be explained using model theoretic tools;

*"On algebraic closure in pseudofinite fields," by O. Beyarslan and E. Hrushovski;
etc.
Also, there is a recent book Model Theory with Applications to Algebra and Analysis: v. 1 (LMS Lecture Note series v. 349, Cambridge, 2008) which would probably be very relevant (judging by the table of contents -- unfortunately I haven't had a chance to read it yet).
A: I like what I've heard about this 2005 GAFA paper on topological dynamics by Kechris-Pestov-Todorcevic:
Link
It uses the Fraïssé limit construction to produce a family of topological groups with interesting universal minimal flows.
A: *

*For a particular result in analysis with a snappy non-standard proof, there's this proof of the Bieri-Groves Theorem on tropical amoebas.  (Does this count as "analysis"?  I'm not sure.)

*There are some nice applications of model theory to [differential Galois theory],2 partly due to the fact that the complete theory of differentially closed fields of characteristic zero happens to have extremely nice model theoretic properties (it's omega-stable, hence there nice rank functions on definable sets and unique-up-to-isomorphism prime models over any set of parameters).
A: There is a proof of a p-adic birational version of Grothendieck's Section Conjecture by Jochen Koenigsmann using Model theory: https://arxiv.org/abs/math/0305226
I'm not entirely sure, but I think there is no known (published?) proof of this result not using model theory.
A: Two more examples of applications:
The paper by Hrushovski arXiv:math/0406514v1 gives an application of Model Theory to a conjecture by Jacobi on difference equations.
The paper by Cluckers, Hales and Loeser arXiv:0712.0708 gives an application of Model Theory to the Fundamental Lemma in Langlands Theory.
A: *

*I think the Manin-Mumford Conjecture proofs first used some methods of Model theory, before it was finally proved by Raynaud. I am not able to dig up references, though.


*Yuri Manin and people who worked in relation with him, posted many papers on arXiv relating the problem of getting Mordell-Weil type theorems in higher dimensions, i.e., on cubic surfaces etc.. One of the references is https://arxiv.org/abs/1001.0223
A: Don't forget the beautiful theory of motivic integration, initiated by Maxim Kontsevich at an Orsay seminar, and developed by Jan Denef, François Loeser, Raf Cluckers, Julien Sebag and many others. The theory is becoming increasingly important.
The crucial, first paper by Denef and Loeser:
Denef & Loeser, 
"Germs of arcs on singular algebraic varieties and motivic integration" (Inventiones Mathematicae 1999)
Another standard reference which should be readable - "In writing the paper we tried our best keeping it accessible to a wide audience including algebraic geometers and model theorists":
Cluckers & Loeser, 
"Constructible motivic functions and motivic integration" (Inventiones Mathematicae 2008)
A very nice overview of some applications:
Loeser's slides for his ECM plenary lecture
A: Recently Pillay and his student Nagloo tackled transcendence questions about the famous Painlevé equations. They entirely use model theory:
Nagloo and Pillay - On algebraic relations between solutions of a generic Painlevé equation
Nagloo and Pillay - On the algebraic independence of generic Painlevé transcendents
A: Sorry to dig up such an old question, but I wanted to mention some more applications of Model theory that has perhaps been not covered in the other answers:
1) Using the basic algebraic fact that given a field $\mathbb F$ and finitely many polynomials $f_1,...,f_n \in \mathbb F[X]$, there is a field extension $\mathbb K_{|\mathbb F}$ in which all the $f_i$ s has a root; one can show by using the Compactness theorem  , that given a field $\mathbb F$, there is a field extension $\mathbb L_{|\mathbb F}$ in which every polynomial $f \in \mathbb F[X]$ has a root. This in turn can be used iteratively to build an algebraically closed field extension $\mathbb K_{|\mathbb F}$ . Then taking the field of all elements of $\mathbb K$ which are algebraic over $\mathbb F$, we get an algebraic extension of $\mathbb F$ which is algebraically closed i.e. we get an algebraic closure of $\mathbb F$. The Compactness theorem can also be used to prove the uniqueness of algebraic closure. 
2) The first order theory of Real Closed fields in the language of ordered fields has quantifier elimination. This can be easily used to prove certain facts about " semi-algebraic sets" (i.e. sets which are Boolean combination i.e. finite union , intersection and compliment of sets of the form $\{\bar x : p(\bar x) =0\}$ and $\{\bar x : p(\bar x) <0\}$, where $<$ is the canonical order on a real closed field and $p$ is a multivariate polynomial with coefficients in the field)  
(i) If $\mathbb F$ is a real closed field and $f: \mathbb F^m \to \mathbb F^n$ is a semi-algebraic function (the graph of the function is a semi-algebraic set) , then $f(A)$ and $f^{-1}(B)$ are semi-algebraic for any semi-algebraic sets $A \subseteq \mathbb F^m ,  B\subseteq \mathbb F^n$. This is often called the generalized Tarski-Seidenberg theorem.
(ii)  Every non-negative element in a real closed field is the square of a unique non-negative element; this defines the square root of a non-negative element. For a real closed field $\mathbb F$, using the $\mathbb F$-valued norm $|(x_1,...,x_n)|:=\sqrt {x_1^2+...+x_n^2}$ on $\mathbb F^n$ , we get a topology on $\mathbb F^n$. Using quantifier elimination, it can be easily shown that the closure (under the above mentioned topology) of any semi-algebraic set is again semi-algebraic. 
(iii) the theory of RCF has quantifier elimination and has a prime model, hence it is a complete theory. Using this it can be shown that If $\mathbb F$ is a Real closed field and $f : \mathbb F^m \to \mathbb F^n  $ is a continuous (w.r.t. the topology ) semi-algebraic function, then $f$ carries closed and bounded sets to closed and bounded sets (bounded in the sense of the $\mathbb F$-valued norm). 
(iv) Using the completeness of RCF and quantifier elimination , it can also be shown that if $f: \mathbb F \to \mathbb F$ is semi-algebraic , then for any open-interval $U\subseteq \mathbb F$, there is $x \in U$ such that $f$ is continuous at $x$. 
And there are many more similar results. 
A: Plane geometry is decidable. That is, we have a computable algorithm that will tell us the truth or falsity of any geometrical statement in the cartesian plane. 
This is a consequence of Tarski's theorem showing that the theory of real closed fields admits elimination of quantifiers. The elimination algorithm is effective and so the theory is decidable. Thus, we have a computable procedure to determine the truth of any first order statement in the structure (R,+,.,0,1,<). The point is that all the classical concepts of plane geometry, in any finite dimension, are expressible in this language. 
Personally, I find the fact that plane geometry has been proven decidable to be a profound human achievement. After all, for millennia mathematicians have struggled with geometry, and we now have developed a computable algorithm that will in principle answer any question. 
I admit that I have been guilty, however, of grandiose over-statement of the situation---when I taught my first logic course at UC Berkeley, after I explained the theorem some of my students proceeded to their next class, a geometry class with Charles Pugh, and a little while later he came knocking on my door, asking what I meant by telling the students "geometry is finished!". So I was embarrassed.
Of course, the algorithm is not feasible--its double exponential time. Nevertheless, the fact that there is an algorithm at all seems amazing to me. To be sure, I am even more surprised that geometers so often seem unaware of the fact that they are studying a decidable theory.
A: Try looking at at a nice short introduction to "modern" "applied" model theory. 
Perhaps it could be used to prepare to teach a short course on "applied model theory" at UGA this summer.
A: Hilbert's Nullstellensatz is a consequence of the model completeness of algebraically closed fields.
Edit: I don't have a reference, but I can sketch the proof. Suppose you have some polynomial equations that don't have a solution over ${\mathbb C}$. Extend ${\mathbb C}$ by a formal solution, and then algebraically close to get a field $K$. The field $K$ obviously contains a solution, but by model completeness of algebraically closed fields, a first-order statement is true in an algebraically closed field only if it is true in every algebraically closed subfield that contains all its parameters. The existence of a solution to a finite set of polynomial equations is a first-order statement (whose parameters are the coefficients) and ${\mathbb C}$ is algebraically closed. QED.
A: Not sure if this is what you are looking for but Tychonoff's theorem has a snappy two line proof in the non-standard setting once the non-standard characterization of compact is established. The non-standard characterization of compactness says that $X$ is compact if and only if every $x\in X^*$ is infinitely close to some standard point in $X$ and infinitely close is defined in terms of the monads of the topology.
Edit: (Tychonoff) $X := \prod_{i\in I}X_i$ is compact if and only if each $X_i$ is compact.
The forward direction is easy and does not require any non-standard analysis. Simply use the projection maps.
Now suppose all the $X_i$ are compact and let $y\in X^*$ then $y(i^*)\in (X_i)^*$. Since $X_i$ is compact there is some $x(i)\in st(y(i^*))$ and we can take $x\in X$ to be the product of the points $x(i)$. By construction $x^*\approx y$ and this establishes the backward direction.
The above theorem along with its non-standard proof can be found in "Nonstandard Analysis" by Martin V$\ddot{a}$th on page 166 but I'm sure any other book on the subject will include a proof of the theorem using pretty much the same terminology and concepts.
Notation: $(-)^*$ is the extension map, $st(-)$ is the standard part map, and $\approx$ is the relation defined in terms of the monads of the topology.
A: You can prove Gromov's Theorem on groups of polynomial growth. See ven den Dries and Wilkie, Gromov's theorem on groups of polynomial growth and elementary logic, J Algebra, 89 (1984), 391-396.
A: I guess this one is a bit too late for this summer, but the theory of o-minimal structures greatly simplified proofs in real algebraic and subanalytic geometry, by emphasizing concepts over nitty-gritty details (at the cost of a loss of constructivity, of course, but what can you expect?).
It is worth noting that these two structures are the ones for which the o-minimal property was known before the notion itself was formalized.  Many more have been discovered since then, the most noteworthy being probably the real exponential field (Wilkie).
A: Alan Dow and others have explored the use of elementary submodels in Topology. See e.g. his introductory paper here or here. One application: the theorem by Arhangel'lskij that a Hausdorff Lindelöf first countable space is at most size continuum. There is a technical proof using transfinite recursion (the standard one), but also a slick one using elementary submodels (of sufficiently large countable models of ZFC).
A: There are many results in Banach space theory that are proved via ultraproducts or non standard hulls, and most books on the subject contain a few.  One nice one that is easy to state is that a Banach space that is uniformly homeomorphic to a Hilbert space is linearly homeomorphic to a Hilbert space.
