Many-Sorted First-Order Model Theory

Abstract

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 M is the class of all models of a set F of formulas, we say that F is a `theory' of M; 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 unit disk and interpret a line as a diameter or a circular arc orthogonal to the boundary. In this model (known as the Poincaré disk) the first four postulates hold but not 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. Another important feature is that we will consider first-order structures with empty carrier sets following Wilfrid Hodges' approach in a A Shorter Model Theory, thus allowing for higher mathematical flexibility on the objects our logical languages describe. Many-sorted first-order structures can be regarded as models of concrete software systems. 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.

Tomasz Kowaslki's website for model theory

Contents

1. Introduction of many-sorted first-order logic (models, sentences and satisfaction relation), and basic logical concepts (substitutions, reachable models and proof rules). The main result delivered here is Gödel's completeness --- every semantic consequence has a proof.

Lecturer: Daniel Găină

Lecture notes (updated on June 3)

2. A characterization of elementary equivalence by Ehrenfeucht-Fraïssé games, commonly known as Fraïssé-Hintikka Theorem. Since finite games are quite intuitive and easy to describe, Fraïssé-Hintikka Theorem gives a better handle on elementary equivalence than Keisler-Shelah Theorem characterizing elementary equivalence via ultrapowers.

Lecturer: Tomasz Kowalski

3. The relationship between gaining expressive power in extending first-order logic and losing some of its important properties. A paramount result in this direction is Lindström’s theorem, which characterizes first-order logic among its extensions by two major properties: the Downward Löwenheim-Skolem Property and Compactness. In any proper extension of first-order logic at least one of the two fails.

Classes

1. May 13, 16:00 ~ 18:00, W1-D710
2. May 20, 16:00 ~ 18:00, W1-D710
3. May 27, 16:00 ~ 18:00, W1-D710
4. June 3, 16:00 ~ 18:00, W1-D710
5. June 10, 16:00 ~ 18:00 (online only)
6. June 17, 16:00 ~ 18:00 (online only)
7. June 24, 16:00 ~ 18:00 (online only)
8. July 1, 16:00 ~ 18:00 (online only)
9. July 8, 16:00 ~ 18:00 (online only)
10. July 15, 16:00 ~ 18:00 (online only)
11. July 29, 16:00 ~ 18:00 (online only)
• Zoom
• Passcode: same as for lecture 1