Finite model theory
Code  Completion  Credits  Range 

NIFMT  Z,ZK  4  2P+1C 
 Garant předmětu:
 Lecturer:
 Tutor:
 Supervisor:
 Department of Theoretical Computer Science
 Synopsis:

The aim of the course is to introduce students to the basics of finite model theory. The original motivation is the questions expressibility and verifiability of logical properties of database systems. Since its inception in the 1970s, the course has evolved rapidly and touched on many other areas of theoretical computer science, such as descriptive complexity theory, the Constraint Satisfaction Problem (CSP), the theory of algorithmic metatheorems and combinatorics.
 Requirements:

The student is assumed to be familiar with standard basic courses of theoretical computer science at FIT CTU such as discrete mathematics and logic (BIEDML) and graphs and algorithms (BIEAG1).
 Syllabus of lectures:

1. Course overview, motivation and relation to the theory of database systems [L][FE][G&al]
We review the basics of mathematical logic and its relationship to expressing properties of graphs and relational structures and explain how database systems can be described as finite relational structures. We also explain the limitations of logic on finite structures.
2. EhrenfeuchtFraı̈ssé games [L, Chapter 3]
We introduce the EhrenfeuchtFraı̈ssé (EF) games as one of the basic tools of model theory. As an
example, we also discuss the problem of isomorphism and logical equivalence of two finite structures.
Next, we show the first restriction, on the number of rounds, which identifies a fragment of the firstorder
logic on formulas of bounded quantifier depth.
3. Inexpressibility theorems in firstorder logic [L, Ch. 3].
An important application of the EF games is in showing whether a given property of graphs or relational structures is expressible in firstorder logic. We explain and demonstrate this technique with examples.
As a motivating example we show that connectedness is not expressible in firstorder logic.
4. Hanf's locality theorem [FE, ch. 2]
We state and prove Hanf's locality theorem and its threshold variant, the FaginStockmeyerVardi theorem. We will show that the inexpressibility of connectedness also a direct consequence of this theorem, and we will add other consequences of inexpressibility, such as parity.
5. Gaifman's locality theorem [FE, ch. 2]
To motivate Gaifman's theorem, we show examples where we cannot make use of Hanf's theorem.
We introduce the construction of a Gaifman graph to a given relational structure and prove Gaifman's theorem.
As an application, we show the AjtaiGurevich theorem.
6. Descriptive complexity and secondorder logic [L, Ch. 6,9]
We explain the relationship between logic and computational complexity. We discuss the relationship of firstorder logic and the computational class PTIME. Next, we state Fagin's theorem, expressing that the existential secondorder logic corresponds to a complexity class NP. We also mention the extension of firstorder logic to fixpoint operators and the corresponding computational complexity.
7. Logics with the ability to calculate [L, ch. 8]
We introduce the bijective EF games and extend firstorder logic with quantifiers expressing the number of satisfiable assignments, and prove the relation between the winning strategy in the bijective EF game and the corresponding logical equivalence. We analyze the algorithmic power of counting quantifiers.
8. Turing machines and finite models [L, Ch. 9].
We prove Trakhtenbrot's theorem and the failure of compactness on finite models. We also discuss other theorems from infinite model theory and their restrictions to finite structures. The main positive example will be Rossman's Homomorphism Preservation Theorem.
9. Logics with a finite number of variables [L, Ch. 11]
We introduce pebble games and show their correspondence with fragments of logics with a restricted number of variables. We will discuss the connection with the extension to counting quantifiers. Finally, we show that, despite the inability to express connectedness, the (logical) logical theory of a structure can help to identify connectedness or different types of disconnectedness.
10. Constraints satisfaction problem and logic [G&al, ch. 6].
We explain the relation between the Constraints Satisfaction Problem and the problem of existence of homomorphisms. Using the ChandraMerlin correspondence, we translate this problem into the language of existencialpositive logic. We show how the syntactic restrictions on the number of variables and quantifier depth correspond to treewidth and treedepth.
11. Game comonads and oneway games [AS][ADW]
We introduce oneway games and show their correspondence with existencialpositive fragments. We motivate comonads as encodings of oneway EF and pebble games. We show that such encodings satisfy the axioms of comonads.
12. Coalgebras of game comonads [AS][ADW]
We introduce the notion of coalgebras and explain the relationship of coalgebras of our comonads to the combinatorial properties of treewidth and depth.
13. Game Comonads and Logic [AS][ADW]
We will uniformly describe bijective and classical forms of EF and pebble games in the category of coalgebras for our game comonads. As an application, we prove some basic theorems from logic using comonads, i.e. without having to work with the syntactic description of the logic in question.
 Syllabus of tutorials:

1. Exercises from EhrenfeuchtFraı̈ssé games for deciding or disproving logical equivalence.
2. Consultation on the term paper, determination of the topic of the paper.
3. Exercises on locality theorems as a tool for proving winning strategies of the Duplicator in EF games.
4. Consultation on the term paper, focusing on discussion of the assigned literature.
5. Exercises on variants of EF games and especially their relation to different fragments of firstorder logic.
6. Consultation on the term paper, discussion of the content of the text.
7. Exercises on game comonads + credit test
 Study Objective:
 Study materials:

[L] Leonid Libkin. Elements of Finite Model Theory. SpringerVerlag 2004.
[FE] HeinzDieter Ebbinghaus, Jörg Flum. Finite Model Theory: Second Edition. SpringerVerlag 1995.
[T] Szymon Toruńczyk. Lectures on Finite Model Theory, University of Warsaw, 2022.
https://duch.mimuw.edu.pl/~szymtor/fmt.pdf
[G&al] Erich Gradel, Phokion Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y Vardi,
Yde Venema, Scott Weinstein. Finite Model Theory and Its Applications. SpringerVerlag 2007.
[AS] Samson Abramsky, Nihil Shah. Relating Structure and Power, Comonadic Semantics for
Computational Resources. Journal of Logic and Computation, 2021.
[ADW] Samson Abramsky, Anuj Dawar, Pengming Wang. The pebbling comonad in Finite Model
Theory. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2017.
 Note:
 Further information:
 https://courses.fit.cvut.cz/NIFMT
 No timetable has been prepared for this course
 The course is a part of the following study plans:

 Master specialization Computer Science, in Czech, 20182019 (elective course)
 Master specialization Computer Security, in Czech, 2020 (elective course)
 Master specialization Design and Programming of Embedded Systems, in Czech, 2020 (elective course)
 Master specialization Computer Systems and Networks, in Czech, 202 (elective course)
 Master specialization Management Informatics, in Czech, 2020 (elective course)
 Master specialization Software Engineering, in Czech, 2020 (elective course)
 Master specialization System Programming, in Czech, version from 2020 (elective course)
 Master specialization Web Engineering, in Czech, 2020 (elective course)
 Master specialization Knowledge Engineering, in Czech, 2020 (elective course)
 Master specialization Computer Science, in Czech, 2020 (elective course)
 Mgr. programme, for the phase of study without specialisation, ver. for 2020 and higher (elective course)
 Study plan for Ukrainian refugees (elective course)
 Master specialization System Programming, in Czech, version from 2023 (elective course)
 Master specialization Computer Science, in Czech, 2023 (elective course)