In model theory, a model is the semantic half of the semantics/syntax separation theme that model theory exists to promote. The syntatical half is called a language, almost always a formal language. As rp wrote long, long ago, "Semantics is another word for meaning." A model of a particular language gives meaning to utterances expressed in that language.

Models in natural languages

"What's in a name? That which we call a rose
By any other name would smell as sweet." — Romeo and Juliet II.I

Shakespeare knew a thing or two about semantics. Whatever word we use to mean "a flower of genus Rosa," they all refer to the same object in the 'real world'. In a sense, the 'real world' is a model for our human language. The main drawback with this analogy is that all human languages are by nature inexact, so we can have utterances that don't make any sense, like "Colorless green ideas sleep furiously", and utterances that aren't well-defined, like "I talked about sex with your grandmother."

This makes translation an art, not a science.

Models for formal languages

In a formal language, we can avoid this ambiguity and construct models where there is only one interpretation (a truth value) for a given utterance. This usually means developing an inductive definition for well-formed formula (a.k.a., wff) and then defining a model using that definition so that truth values respect logical operators. For example, in propositional logic, one can define wff like so:

• If A is a bare propositional variable or one of the constants True, False, then A is a wff.
• If A is ¬B, where B is a wff, then A is a wff.
• If A is B ∨ C, where B and C are wffs, then A is a wff.

And then one can define the logical operators by forcing models of propositional logic to respect them. So one could define a model of propositional logic to be a function from wffs to truth values such that:

• If A is a propostional variable, then it is either True or False. Tertium non datur.
• If A is ¬ B, then A has the opposite truth value of B.
• If A is B ∨ C, then A is true if and only if at least one of B or C is true.

More complicated logics and languages have accordingly more complicated definitions, but they work relatively the same way. A model in first-order logic, for example, should be able to support function symbols, predicates, and at least the universal quantifier. This type of thing has been developed better elsewhere.

Once the foundations of first-order model theory are set up, a great deal of very cool things can be done. The ultraproduct and Los' theorem can be used to prove some seriously awesome theorems in other parts of mathematics (what model theory calls 'theories'), and they can also be used to build one school of non-standard analysis. The compactness theorem is another result of model theory that lends itself well to a whole slew of problems, as the writeup for it indicates.

The mathematical portion of this was developed along the lines described in C. Chang's Model Theory.