What's the difference between predicate logic and model theory?

Question

I studied model theory a little bit, and now that I'm reading the Wikipedia aricle on predicate logic, it seems to me that this is precisely model theory in that there is also the notion of signature (as in model theory), predicate (relation) symbols, function symbols, etc.; and terms, formulas are defined in the same way.

So I was wondering what's the difference between predicate logic and model theory? Is model theory a generalization of predicate logic?

Answer 1

As pointed out in the comments, predicate logic is an object of study, while model theory is a discipline, or a way to approach an object of study. The easiest way to see the difference is to compare model theory to other disciplines, and the (most prominent, if not only) alternative way to study FOL is proof theory. Model theory and proof theory are historically in a kind of opponent relation to each other, although they don't exclude each other, it's just two different ways of studying the same formal language.
"Proof" as in "proof theory" is to be understood not as a mathematically flavored English text like "Suppose $\phi$ is false. Since, by Lemma 3.2, ...", but as a formal proof in some system like natural deduction, sequent calculus, Hilber-style calculus, ..., i.e. a system of rules for manipulating strings of symbols. One such rule could be "If you have a symbol $\phi$ and you have another symbol $\psi$ next to it, then you are allowed to draw a line under them, label that line with "($\land I$)" and write $\phi \land \psi$ underneath that line" (this would be the conjunction introduction rule in a Gentzen-style natural deduction system). Proofs are syntactic objects which are precisely defined by a set of rules on how to manipulate strings of formulas, without any assumptions about interpretations in a model.

While model theory asks whether a formula is true in a particular model/under a particular interpretation of the non-logical symbols, what properties a model of some formula has (for example, whether its domain is finite or infinite), or whether two models are isomorphic, proof theory asks whether a formula is derivable in some formal proof system, what properties a possible proof has (for example, whether it's normalizable, or whether it satisfies the subformula principle), or whether two proofs for a formula are the same (modulo some syntactic transformations). While model theory would say "The meaning of '$\phi \to \psi$' is that if $\phi$ is true under a valuation and interpretation in some model, then $\psi$ must hold as well under that valuation in this model", proof theory would say "The meaning of $\phi \to \psi$ is that, if, given a $\phi$ as a premise, I can derive a proof of $\psi$, then I am allowed to wirte $\phi \to \psi$ as a conclusion, and can strike through the assumption $\phi$ to mark it as discarded." Although "formal proof" is often understood as a syntantactic notion while "truth" or "semantics" is reserved for models, proof-theoretic semantics argues that the meaning, i.e. the semantics of FOL objects like connectives can be defined in terms of formal proof systems, and not just with respect to models.

So model theory, just like proof theory, is one way of invastigating predicate logic, which is the subject of study.