Model Theory

Many-Sorted First-Order Model Theory


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)

Tomasz Kowaslki's website for model theory

Classes (via Zoom)

  1. May 7 (16:00~18:00) Lecture 1 - pdf video (Agps*dNsZDj8)
  2. May 14 (16:00~18:00) Lecture 2 - pdf video
  3. May 21 (16:00~18:00) Lecture 3 - pdf video
  4. May 28 (16:00~18:00) Lecture 4 - pdf video
  5. June 4 (16:00~18:00) Lecture 5 (by Tomasz Kowalski) - pdf video
  6. June 11 (16:00~18:00) Lecture 6 (by Tomasz Kowalski) - pdf video (VkHv#Y2s69mM)
  7. June 18 (16:00~18:00) Lecture 7 (by Tomasz Kowalski) - pdf video (Q1Nrea^7Urou)
  8. June 25 (16:00~18:00) Lecture 8 (by Tomasz Kowalski) - pdf video (eCk@GfZJar8C)
  9. July 2 (16:00~18:00) Lecture 9 (by Tomasz Kowalski) - pdf video (8GjUYqo3vm=U)
  10. July 9 (16:00~18:00) Lecture 10 (by Tomasz Kowalski) - pdf video (C6Sm3px6r+ra)
  11. July 16 (16:00~18:00) Lecture 11 (by Tomasz Kowalski) - pdf video (1nJMj5pAr#g9)
  12. July 23 (16:00~18:00) Lecture 12 (by Tomasz Kowalski) - pdf video (L!wyb917XHe1)