Wikipedia defines model theory as …
… the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models, taken as interpretations that satisfy the sentences of that theory.
Why does this field need to exist? If we have proof theory, then we can discuss any formal system $\Gamma$ and statements within $\Gamma$ like, say, some arbitrarily chosen sentences $\phi$ and $\psi$, and even theorems like $\Gamma \vdash \phi \to \psi$, assuming that $\psi$ is derivable from $\phi$ in $\Gamma$, of course. Why should anyone care whether $\Gamma \models \phi$ if one already knows that $\Gamma \vdash \phi$?
Thanks for any advice.
Best Answer
Model theory is an excellent tool for talking about the semantics of formal languages, particularly first order logic with equality and with constants, functions and non-logical predicates, by building models out of sets. You can do other, fancier things with it like considering models of set theory itself, but I don't understand those applications and can't comment on them.
One interesting fact from model theory is the existence of nonstandard models of arithmetic. I think this is a good motivating example because it shows that axiomatizations of seemingly simple things like arithmetic do not pin down a semantics as much as we would like.
I can try to answer this from the perspective of someone who found out about model theory through the proof theory and programming language theory route. I don't know the subject well; I'm just a beginner. As a meta note, I think Noah Schweber is right and you should phrase your question more politely.
Basically, a model is a structure that assigns interpretations to various symbols and has a domain of discourse. The interpretations are all drawn from our universe of sets in our underlying set theory.
A symbol is an abstract component in a signature. It can be a constant symbol (like a nullary function), a function symbol, or a predicate symbol. Functions and predicates can have different arities. Normally, there's a single domain of discourse, but you can generalize this to multiple sorts if you want to.
So, symbols in signatures can be used in two ways. They can be used in your formal language. For instance, if $f$ is a function symbol, you can express properties about $f$ in your language.
$$ \forall x \mathop. \forall y \mathop. f(x, y) = f(y, x) $$
The function symbol $f$ is also supplied an interpretation in a given structure.
A set of sentences using non-logical symbols taken from a particular signature can be used to define a theory. A structure where all the sentences in a theory are true is called a model of the theory.
But, structures are also made of sets. This means that their domains have cardinalities.
This means that you can talk about the spectrum of a theory, which is the number of models up to isomorphism for each cardinality.
The two results that Noah Schweber mentioned in a comment constrain the shape of spectra of a theory for infinite cardinalities. NOTE: I'm counting models up to isomorphism here, not "raw" models.
The Löwenheim–Skolem theorem says that if your theory has an infinite model, it has at least one model of every infinite cardinality.
Morley's categoricity theorem says that if your theory has exactly one infinite model for some uncountable cardinality $\kappa$, then it has exactly one infinite model for all uncountable cardinalities.