Elementary (i.e. first-order) theories are a key object of study in mathematical logic. Many well-known results are related to the study of algorithmic properties of elementary theories of different classes of structures (graphs, groups, lattices, rings, etc.) and their fragments.

One of the most important methods for proving algorithmic decidability for elementary theories is the method of quantifier elimination. In particular, it was used to obtain proofs of the decidability of the theories of two fundamental structures:

(1) the ordered group of integers under addition;
(2) the ordered field of real numbers.

On the other hand, decidable theories are relatively rare; most theories turn out to be undecidable. For example, Gödel's first incompleteness theorem (in Rosser's form) implies the undecidability of the theory of discretely ordered rings, as well as all its consistent supertheories. Another striking example is the undecidability of the theory of finite simple graphs and all its subtheories. To transfer undecidability results from theories to other theories, the method of interpretation is used. In particular, using this method one can pass from simple graphs to symmetric groups or distributive lattices.

The aim of the present course is to introduce students to the methods mentioned above and their applications in the study of elementary theories.

Course program

1. A brief introduction to classical first-order logic.
2. A brief introduction to computability theory. Encoding formulas and theories.
3. The method of quantifier elimination. The decidability of the theory of dense linear orders without endpoints; related results on definability and axiomatization.
4. The decidability of the theory of the ordered group of integers under addition; related results on definability and axiomatization.
5. The decidability of the theory of the ordered field of real numbers; related results on definability and axiomatization.
6. The strong undecidability of the theory of discretely ordered rings. Other decidability and undecidability results related to rings and fields.
7. The method of interpretation (relative elementary definability). Hereditary undecidability of theories of different classes of structures (graphs, groups, lattices, etc.) and their fragments.
8. Degrees of undecidability of theories.

Main references
[1] Yu.L. Ershov, I.A. Lavrov, A.D. Taimanov, M.A. Taitslin, Elementary theories. Russian Mathematical Surveys, 20 (1965), 35–105.
[2] P.J. Cohen, Decision procedures for real and p-adic fields. Communications of Pure and Applied Mathematics, XXII (1969), 131–151.
[3] H.B. Enderton, A Mathematical Introduction to Logic. 2nd ed. Academic Press, 2001.
[4] A. Nies, Undecidable fragments of elementary theories. Algebra Universalis, 35 (1996), 8–33.
[5] H. Rogers, Jr., Theory of Recursive Functions and Effective Computability. McGraw-Hill, 1967.
[6] A. Tarski, A Decision Method for Elementary Algebra and Geometry. 2nd ed. University of California Press, 1951.
[7] A. Tarski, A. Mostowski, R.M. Robinson, Undecidable Theories. North-Holland Publishing Company, 1971.

Lecturer
Speranski Stanislav Olegovich

Financial support
The course is supported by the Ministry of Science and Higher Education of the Russian Federation (the grant to the Steklov International Mathematical Center, Agreement no.  075-15-2022-265).

Institutions
Steklov Mathematical Institute of Russian Academy of Sciences, Moscow
Steklov International Mathematical Center