I'd just like to expand on John Goodrick's mention of Zilber's work on exponential fields and mention that `Categoricity' of is an active area of research. In particular, model theory may be used to give some justification as to why theorems of classical mathematics should hold.

In general it's an interesting question to see what good model theoretic behaviour translates to in the world of classical mathematics.

One way of viewing things (and this is Zilber's point of view) is that if a mathematical structure is useful, and therfore well studied by the mathematical community, then it will be complicated enough to be interesting, but nice enough to be analysed. One aspect of model theory is involved with trying to classify structures with respect to how nice (or wild) they are (e.g. a structure could be strongly minimal, O-minimal, stable, categorical etc...).

At the top of the logical hierarchy sit categorical theories. A theory is $\kappa$-categorical if it has one model up to isomorphism in cardinality $\kappa$. The stereotypical example of a categorical theory is the theory of algebraically closed fields of characteristic $0$. The unique model of cardinality continuum is $\langle \mathbb{C}, + , \cdot , 0,1 \rangle$. This mathematical structure has pretty much every nice model theoretic property that you'd want in a structure - it's strongly minimal (definable sets are very simple i.e. either finite or cofinite), $\omega$-stable (there aren't many types of elements around), homogeneous (you can extend partial automorphisms to automorphisms of the whole structure), saturated (you can realise types - i.e. solutions to polynomials are in there). This theory is also complete and `categorical in powers' i.e. $\kappa$-categorical for every uncountable cardinal.

An amazing theorem of Morley actually says that if a first order theory is $\kappa$-categorical for one uncountable cardinal, then it is categorical for every uncountable cardinal. Morley's theorem (1965) kick started stability theory, and from there Shelah has developed an unbelievable amount of abstract model theoretic technology.

However, after initiating stability theory in the first place it seemed that the study of categorical structures had run its course (Baldwin-Lachlan theorem completely categorises theories which are categorical in powers). But recently Zilber realised that some of Shelah's abstract model theoretic technology regarding infinitary logics can be used to study concrete, well known, and very interesting mathematical structures.

For example, as John Goodrick mentions, if you try and axiomatize the interaction of the exponential function with the complex field i.e. you try and capture the theory of $\langle \mathbb{C},+ \cdot ,0,1, e^x \rangle$, and you want it to be categorical, then you need things like Schanuel's conjecture and the conjecture on the intersections of Tori (CIT) to hold. Along similar lines is the Zilber-Pink conjecture.

So model theory can give us some kind of justification as to why certain results should hold. For example, if you look the theory of the universal cover of a non CM elliptic curve over a number field, and you ask it to be $\aleph_1$-categorical, then it turns out that a famous theorem of Serre saying that the image of the Galois representation on the Tate module is open must be true.