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

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

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

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

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

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

6) Mordell-Lang in positive characteristic (Hrushovski).

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