The use of a model to test for the consistency of an axiomatized system is older than modern logic. Descartes’s algebraic interpretation of Euclidean geometry provides a way of showing that if the theory of real numbers is consistent, so is the geometry. Similar mappings had been used by mathematicians in the 19th century, for example to show that if Euclidean geometry is consistent, so are various non-Euclidean geometries. Model theory is the general study of this kind of procedure: the study of interpretations of formal systems. Proof theory studies relations of deducibility between formulae of a system, but once the notion of an interpretation is in place we can ask whether a formal system meets certain conditions. In particular, can it lead us from sentences that are true under some interpretation to ones that are false under the same interpretation? And if a sentence is true under all interpretations, is it also a theorem of the system? We can define a notion of validity (a formula is valid if it is true in all interpretations) and semantic consequence (a formula B is a semantic consequence of a set of formulae, written {A₁…A_n} ╞ B, if it is true in all interpretations in which they are true). Then the central questions for a calculus will be whether all and only its theorems are valid, and whether {A₁…A_n} ╞ B if and only if {A₁…A_n} ⊦ B. These are the questions of the soundness and completeness of a formal system. For the propositional calculus this turns into the question of whether the proof theory delivers as theorems all and only tautologies. There are many axiomatizations of the propositional calculus that are consistent and complete. Gödel proved in 1929 that the first-order predicate calculus is complete: any formula that is true under every interpretation is a theorem of the calculus.