We kindly ask all participants, including remote ones and those
watching recorded videos, to register at this link.
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.
Moreover, from the corresponding proofs one can extract explicit
axiomatizations for both theories and derive interesting results about definability in
(1) and (2).
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
- A brief introduction to classical first-order logic.
- A brief introduction to computability theory. Encoding formulas and theories.
- The method of quantifier elimination. The decidability of the theory of dense
linear orders without endpoints; related results on definability and axiomatization.
- The decidability of the theory of the ordered group of integers under addition;
related results on definability and axiomatization.
- The decidability of the theory of the ordered field of real numbers; related
results on definability and axiomatization.
- The strong undecidability of the theory of discretely ordered rings. Other
decidability and undecidability results related to rings and fields.
- The method of interpretation (relative elementary definability). Hereditary
undecidability of theories of different classes of structures (graphs, groups, lattices,
etc.) and their fragments.
- 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.
 RSS: Forthcoming seminars
 Lecturer
Speranski Stanislav Olegovich
Organizations
Steklov Mathematical Institute of Russian Academy of Sciences, Moscow
Steklov International Mathematical Center |
