The course is an introduction to model theory: a branch of mathematics that deals with the classification of structures by means of logical formulas. Mathematical structures (groups, rings, fields, ordered sets, lattices, and others) can be classified according to the logical formulas that are true in them. Conversely, given some logical formulas, one wants to find classes of structures in which the formulas are true. We call those structures `models' of the formulas; moreover, when S is the class of all models of a set F of formulas, we say that F is a `theory' of S; hence, the name of model theory. Historically, mathematicians have used models all the time, they just did not build a theory around it. For example, to demonstrate that Euclid's fifth postulate does not follow from the rest, one can take a sphere: a (non-standard) model of all the postulates except the fifth. Model theory however is relatively young, it did not exist before the second half of the 20th Century.
In addition, this course provides the foundations of software specification and formal verification of systems from the perspective of the work on algebraic specification. It also introduces some basic concepts necessary for the design of an algebraic-specification language. One important characteristic of the present course is the use of many-sorted first-order structures (instead of single-sorted structures), which consist of collections of sets (of data values) together with functions and relations over those sets. Each such structure can be regarded as a model of a concrete software system. Therefore, we can learn a lot about software systems by analyzing their model theory. This abstraction corresponds to the view that the correctness of the input/output behaviour of a software system takes precedence over other properties such as efficiency.Lecture notes (previous version)