Spring term 2024/25, course code NMAG570, Wednesday 10:15, Institute of Mathematics (Žitná 25), Blue lecture room (ground floor at the rear building)
Consultations: drop me an email to arrange a meeting
Syllabus
We will study basic methods for proving algorithmic decidability of first-order theories and main examples of
decidable theories.
Tools:
- quantifier elimination
- interpretations
- Fraïssé limits
- Ehrenfeucht–Fraïssé games
- Feferman–Vaught-like theorems
Exhibits (depending on time constraints):
- algebraically closed and real-closed fields
- theories of linear orders
- theories of Boolean algebras
- theories of random structures and locally free algebras
- theories of abelian groups and modules
- ordered abelian groups (divisible, Presburger arithmetic)
- Skolem arithmetic
This lecture in spring term 2023/24
Exam
There will be an oral exam assessing understanding of the main results presented during the course. Each student will present one of the main topic groups of their own choosing.
The list of possible topics in 2023/24 was as follows, but this is subject to change depending on what exactly we will cover in the course this year:
- Syntactic and semantic criteria for QE. Algebraically closed fields.
- Fraïssé limits. Either random graphs or atomless Boolean algebras.
- Ehrenfeucht–Fraïssé games, graded back-and-forth systems. Presburger arithmetic.
- The theory of linear orders.
- Feferman–Vaught theorems. Skolem arithmetic.
Recommended literature
- Wilfrid Hodges, Model Theory, Cambridge University Press, 1993
- Michael O. Rabin, Decidable theories, in: Handbook of Mathematical Logic (ed. Jon Barwise), 1977, §C.3, pp. 595–629.
- Hans Läuchli, John Leonard, On the elementary theory of linear order, Fundamenta Mathematicae 59 (1966), no. 1, pp. 109–116. See also A note on the theory of well orders.
NB: Excepting the Note, these electronic materials are provided strictly for individual study purposes, not for further distribution; I hold no copyrights to them.
Lectures
#1 (21 Feb 2025)
- Decidable and recursively axiomatizable theories.
- Quantifier elimination and decidability.
- Syntactic QE sufficient condition.
#2 (26 Feb 2025)
- Syntactic QE example: discrete linear orders.
- Model-theoretic QE example: dense linear orders.
- Substructures, embeddings, diagrams.
#3 (5 Mar 2025)
Plan:
- Criterion for quantifier elimination.
- Example: QE for algebraically closed and real-closed fields.