This is a subject taught jointly with Daniel Gaina from Kyushu University. We try to cater for two types of audience:
Computer scientists with strong interest in foundations of specification and verification languages.
Mathematicians with some interest in logic and foundations.
The result is probably somewhat incoherent, but we hope that next iterations will make it less so. Here is a short description of the subject.
Model theory is a branch of mathematics that deals with classifying structures by means of logical formulas that are true in them. At this vague level it can well be said of mathematics as a whole - what makes model theory special is that the formulas as well as structures are treated with particular care. Here is an example. Consider Euclid's Fifth Postulate: "That, if a straight line falling on two straight lines make the interior angles on the same side less than two right angles, the two straight lines, if produced indefinitely, meet on that side on which are the angles less than the two right angles". Or in a more modern version: for every line L and every point P not on L line there exist precisely one line through P not intersecting L. For about two thousand years mathematicians tried to show that the fifth postulate can be derived from the others. They failed. Then Riemann (let's say) comes along and says: hey, what if lines were great circles instead? Then all the other postulates hold, but the fifth fails miserably. So it cannot be derived from the others: if it could, it would hold in all situations in which all the others hold. End of story.... you may wonder why it took so long. And quite possibly it took so long because the distinction between a statement about a structure (such as the fifth postulate) was not clearly separated in the minds of mathematicians from the structure itself. One thing model theory does is precisely that. Typical questions arise. If one model and another satisfy precisely the same statements in some formal language, must they be isomorphic? What is a good notion of morphism between models? If a class of models is closed under something, is it reflected in the formulas we use to talk about them? It there an algorithm to decide whether a statement holds in a class of structures? And so on. Enough rant.
More precisely, the plan is this:
Begin with introducing a formal language (first-order logic), models (relational structures) and the fundamental relation between them: satisfaction.
Prove completeness of first-order logic: everything that can be derived in a certain proof system (syntactically), can be derived by means of models and satisfiability (semantically). And vice versa. Do everything in the formalism suitable for specification and verification languages, and for abstract analysis of various logical systems. Introduce compactness and demonstrate its usefulness.
Present some preservation theorems, that is theorems of the form: a formula is preserved under some operations on models if and only if it is of certain form (a universally quantified equation, for example).
Introduce ultraproducts: one way of producing non-standard models. Ultraproducts are somewhat out of fashion, but we believe they are still young and fine.
Describe quantifier elimination: how to to prove algorithmic decidability of certain theories by getting rid of quantifiers.
Play games: Ehrenfeucht-Fraisse games, to be precise. Invented to show that some models cannot be distinguished by certain formulas, it is a powerful technique with many applications. Of all model theoretic techniques this alone survives in the finite models.
Homogeneous structures and Fraisse limits will come at the end.