Alfred Tarski and decidable theories. (English) Zbl 0647.03001

Doner, John; Hodges, Wilfrid

J. Symb. Log. 53, No. 1, 20-35 (1988).

Tarski did not invent effective quantifier elimination but he became its master. He used this technique to establish completeness of theories, to classify complete extensions of theories, to identify relations definable in certain theories, and of course to prove decidability of theories. Tarski’s work on linear orders, Boolean algebras, geometry, and fields is summarized. Related results by his students are also noted. A large part of the paper is an interesting scholarly rumination on how Tarski’s views on quantifier elimination evolved. Using Tarski’s writings and reports of his students the authors trace the prewar emphasis on completeness to the postwar concern with “practical” decision procedures. They demonstrate how Tarski, even as he was creating a significant portion of the canon of decidable theories, was limited by the historical context as determined by his predecessors and contemporaries. Yet in the end the breadth of his applications of this one technique had a “deep and cumulative influence on model theory and the logic treatment of algebraic theories”.

Reviewer: J.M.Plotkin

MSC:

03-03	History of mathematical logic and foundations
01A60	History of mathematics in the 20th century
03B25	Decidability of theories and sets of sentences
03C10	Quantifier elimination, model completeness and related topics
03C35	Categoricity and completeness of theories

Keywords:

Tarski; completeness; decidability; linear orders; Boolean algebras; geometry; fields