Alfred Tarski and decidable theories.

*(English)*Zbl 0647.03001Tarski 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