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)
- Criterion for quantifier elimination.
- Example: QE for algebraically closed fields.
#4 (12 Mar 2025)
- Example: QE for real-closed fields.
- Interpretations.
#5 (19 Mar 2025)
- Interpretations of models. Faithful interpretations.
- Example: Euclidean and hyperbolic geometry.
#6 (26 Mar 2025)
- Fraïssé limits.
- Existence of Fraïssé limits.
#7 (2 Apr 2025)
- Uniqueness of Fraïssé limits.
- Extension axioms.
#8 (9 Apr 2025)
- ω-categoricity and QE for Fraïssé limits.
- Example: atomless Boolean algebras.
#9 (16 Apr 2025)
- Ehrenfeucht–Fraïssé games.
- Quantifier rank and k-equivalence.
- Preservation of elementary equivalence.
#10 (23 Apr 2025)
- Graded back-and-forth systems.
- Quantifier elimination using GBFS.
- Example: Presburger arithmetic.
#11 (30 Apr 2025)
Plan:
- Presburger arithmetic (finish).
- Complexity of DLO and Presburger.
- Decidability of the theory of linear orders (start).