Finite model theory, fall 2016
Finite model theory, fall 2016
Teacher: Juha Kontinen and Jonni Virtema
Scope: 10 cr
Type: Advanced studies
Teaching: Four hours of lectures and two hours of exercises per week
Topics: Model theory studies mathematical objects, so-called models, with logical tools. Both algebraic structures, like groups, rings and fields, and objects studied in discrete mathematics, like graphs, trees and linear orderings, are examples of models. The interest in finite models is largely motivated by connections with discrete mathematics and theoretical computer science; therefore one could describe finite-model theory as model theory for discrete mathematics. Classical model theory, on the other hand, studies infinite models almost exclusively, and it is more algebraically oriented.
The course starts with an introduction of the general concept of a model and different ways of measuring the similarity of given models: homomorphisms, isomorphisms and combinatorial games. The close relationship between the games and some logical concepts is studied next. Finite models can also be regarded as inputs to a computer programs (a finite model is practically the same thing as a relational database), which leads to descriptive complexity theory. We will discuss Büchi's Theorem relating monadic second-order logic intimately with finite automata and regular languages. We will also discuss Fagin's theorem characterizing the complexity class non-deterministic polynomial time by existential second-order logic. Time permitting, we will also discuss the zero-one law of first-order logic.
Prerequisites:
Introduction to Logic I&II
The [toc] macro is a standalone macro and it cannot be used inline. Click on this message for details.
News
- The first lecture is on Monday 5 September at 10-12 in room B321.
- The exercise session on Tuesday 22nd of November is cancelled and moved to the next week.
- The last lecture of the course will be on Thursday 8th December.
- The final exam will be organized on Wednesday 21st December at 10-14 in room B321.
- The lecture of Monday 5.12 is cancelled.
Teaching schedule
Weeks 36-42 and 44-49, Monday and Thursday 10-12 in room B321. Two hours of exercise classes per week.
Course diary
Monday 5.9.2016:
- Relations, functions, vocabularies, models, linearly ordered sets, homomorphisms.
Thursday 8.9.2016
- Strong homomorphisms, embeddins, isomorphisms, automorphisms, model reductions, submodels, ordered models. Representation theorem for finite ordered models.
Monday 12.9.2016:
- Partial isomorphisms,
- Terms and atomic sentences.
Thursday 15.9.2016:
- First-order sentences, and quantifier rank of a sentence.
Monday 19.9.2016:
- Infinitary logic and Fraïssé systems.
Thursday 22.9.2016:
- Ehrenfeucht–Fraïssé game.
Monday 26.9.2016:
- Equivalence of Fraïssé systems and Ehrenfeucht–Fraïssé games.
Thursday 29.9.2016:
- Partial isomorphisms up to k equals logical equivalence up to quantifier rank k.
Monday 3.10.2016:
- Pebble game and partial isomorphism up to k variables.
Thursday 6.10.2016:
- Partial isomorphisms up to k variables equals logical equivalence in the k-variable infinitary logic,
- Basic concepts of formal language theory.
Monday 10.10.2016:
- Word models, finite automata, and invariance.
Thursday 13.10.2016:
- Any language L that is a union of equivalence classes of an invariance that has finitely many equivalence classes if recognizable by a finite automaton,
- Definability of languages by logics,
- Second-order logic.
Monday 17.10.2016:
- Fragments of second-order logic,
- Every language recognized by some finite automaton is definable in monadic Σ11.
Thursday 20.10.2016:
- Simulating monadic second-order logic by first-order logic in models with added structure.
Monday 31.10.2016:
- Completed the proof of Büchi's theorem,
- Basics of Turing machines. We follow the textbook of Ebbinghaus and Flum (see ).
Thursday 3.11.2016:
- Complexity classes PTIME, NPTIME and PSPACE,
- Basics of fixed-point logics.
Monday 14 and Thursday 17.11.2016:
- Logical characterization of PTIME, PSPACE and NPTIME by IFP, PFP, and existential second-order logic.
Monday 21.11.2015:
- Satisfiability, validity, and model checking problems. Decidability, undecidability, RE, and coRE.
- Normal form for the one-variable fragment of first-order logic. Notes.
Thursday 24.11.2016:
- Normal form for the two-variable fragment of first-order logic.
- Types.
Monday 28.11.2016:
- Finite model property of the two-variable fragment of first-order logic.
Thursday 1.12.2016:
- Asymptotic probabilities, 0-1 laws, and extension axioms.
Thursday 8.12.2016:
- 0-1 law for first-order logic and FVL.
Final exam
The final exam will be organized on Wednesday 21st December at 10-14 in room B321.
Course material
We will follow the structure of K. Luosto's lecture notes:
Luosto, Äärellisten mallien teoria (in Finnish).
All material covered during the course can be also found in:
Ebbinghaus and Flum, Finite Model Theory.
Other reading:
Väänänen, A Short Course in Finite Model Theory.
The slides of Lauri Hella's summer course in Aix-en-Provence.
Registration
Did you forget to register? What to do?
Exercises
Assignments
Exercise classes
Group | Day | Time | Room | Instructors |
|---|---|---|---|---|
1. | Tuesday | 14-16 | B321 | Juha Kontinen & Jonni Virtema |
Course feedback
Course feedback can be given at any point during the course. Click here.