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

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?

• Model theory is a discipline, predicate logic is an object of study. Analogously: what's the difference between the Euclidean plane and Euclidean geometry? Mar 2, 2019 at 23:36
• I thought predicate logic is also a discipline, just like propositional logic. Does model theory study "predicate logic" then? Mar 2, 2019 at 23:50
• Propositional logic isn't really a discipline either, it's similarly an object of study. Model theory primarily studies predicate logic (or as it's more commonly known these days, "first-order logic") but also studies other logics, including infinitary logic. Mar 3, 2019 at 0:13
• Just to round ot Noah Schweber's comments, predicate logic (and propositional logic) can also be studied from the perspective of proof theory rather than model theory. Model theory is a tool and predicate logic is one of the things you can apply that tool to. There are other things you can apply that tool to as well as other tools. Mar 3, 2019 at 3:42
• @NoahSchweber But "logic" is a discipline, right? It could be a little confusing that logic is a discipline, while predicate logic, second order logic, propositional logic, etc. are objects of study. Same with "algebra" and "topology" and "statistics" which are both disciplines and objects of study.
– bof
Mar 3, 2019 at 4:38

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