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.

- 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)

- 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 - 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.
**Lecturer:**Guillermo Badia

- May 13, 16:00 ~ 18:00, W1-D710
- Zoom
- Passcode: contact the organizer at daniel[at]imi.kyushu-u.ac.jp
- prerequisites
- slides (updated on June 9)
- video (Passcode: 6E&H.bA!)

- May 20, 16:00 ~ 18:00, W1-D710
- May 27, 16:00 ~ 18:00, W1-D710
- June 3, 16:00 ~ 18:00, W1-D710
- June 10, 16:00 ~ 18:00 (online only)
- June 17, 16:00 ~ 18:00 (online only)
- June 24, 16:00 ~ 18:00 (online only)
- July 1, 16:00 ~ 18:00 (online only)
- July 8, 16:00 ~ 18:00 (online only)
- slides (updated on July 12)

- July 15, 16:00 ~ 18:00 (online only)
- July 29, 16:00 ~ 18:00 (online only)
- Zoom
- Passcode: same as for lecture 1