What are some notable contributions of mathematical logic to mathematics (outside of mathematical logic)?

I have been reading an introductory text in mathematical logic (Holden, 1995). The final chapter presents the resolution of Hilberts's tenth problem concerning the integer roots of an arbitrary polynomial over $$\mathbb Z$$.

The resolution (to the negative) follows from a theorem of Yuri Matiyasevich which tells us that every recursively enumerable relation/function is Diophantine.

On the one hand, it is not surprising that a resolution comes via mathematical logic - after all, it is a decidability problem. On the other hand, it is a very natural question with a long history whose resolution is of fundamental importance to Diophantine analysis.

Q: What are some examples of mathematical logic being successfully applied elsewhere?

Rightly or wrongly, I consider set theory to be a part of mathematical logic, so, for example, the CH independence proofs of Cohen and Gödel I am considering to be part of logic.

• See What role has Whiteheads conjecture played in the thinking on the plurality of set theories? and the comments to this question. Jun 26 at 18:10
• Tarski-Seidenberg theorem Image of a (real/complex) algebraic map is semialgebraic: This very useful theorem in algebraic geometry is proven by "quantifier elimination." Jun 26 at 22:28
• @MoisheKohan It is the opposite. Or, equivalenly, this is quantifier elimination. Jun 27 at 19:08
• In which sense is this a question on the history of mathematics? Jul 2 at 5:08

There is a survey of such applications in

Ehud Hrushovski, Geometric model theory. Proceedings of the International Congress of Mathematicians, Vol. I (Berlin, 1998). Doc. Math. 1998, Extra Vol. I, 281–302.

• A whole survey! So not as rare as I had imagined. Unfortunately I am unable to locate a copy of Hrushovski's paper online, and it would likely be well over my head in any case. Do you know if the Dries-Wilkie proof of the (finite version of) Gromov's result (cited in M Sapir's answer) was the first notable application of model theory to geometry? I assume that it is listed in Hrushovski's survey.
– NWR
Jun 28 at 17:25
• mathunion.org/icm/proceedings Jun 29 at 2:19
• Ultrafilters and ultraproducts have been used in Lvov by Banach and others long before Gromov. Jul 1 at 3:54

The van den Dries-Wilkie proof of Gromov polynomial growth theorem is a non-trivial and very fruitful application of logic (model theory to be precise) to group theory and geometry.

• This is a nice example! However, I have a couple of nitpicky points, if I may: The Dries-Wilkie proof appears to be an alternative approach to Gromov's original proof (not that this lessens its importance). The details are a bit over my head but it also appears to deal only with the finite case rather than the full general theorem. Am I reading this correctly?
– NWR
Jun 28 at 17:22
• @Nick: What is "finite case"? They prove the whole theorem (and a little more). Moreover the paper started the theory of asymptotic cones of groups which proved to be very fruitful. Jun 28 at 18:11
• The paper is high level mathematics, the details of which are beyond my current understanding. My reading of the paper was that the authors appeal to model theory and recursion theory in section seven. This section deals only with groups having a finite generating set and begins “Gromov proved also a finite version of his theorem…” As I say, I am probably misunderstanding the details here, but this is what I meant by the “finite case”.
– NWR
Jun 28 at 19:32
• The paper is actually quite easy (and the original Gromov's paper too) modulo big results used there. Now there are alternative proofs which do not use these results (Shalom , Tao and others). If you do not understand the paper, why are you saying that only the "finite case" is proved there? Jun 28 at 20:55