Decidable Logical Theories

Dr. Heinrich Rolletschek

September 29, 2008

Time and place:

Thursday 10:15-11:45, K 112A, beginning October 9.

Entry requirements:

Acquaintance with the most common algebraic structures (groups, lattices etc.); basic knowledge of predicate logic. Results beyond the basics will be given in the lecture.

Course aims:

Students should become familiar with the principal decidability results in the area of logical theories and with the basic methods involved, especially quantifier elimination.

Course description:

A logical theory in the most general sense is any set of sentences (of predicate logic), but this course deals specifically with theories T of the following form: for some class K of models, T is the theory of K, that is, the set of all sentences which are satisfied by every model in K. Such theories turn out to be decidable in various cases of interest, and decision algorithms will be given. A number of general approaches will be introduced, the most important being quantifier elimination.

Chapter 1 uses some very simple logical theories to illustrate the basic method of quantifier elimination, as well as certain model-theoretic methods for proving decidability. Chapter 2 deals with the theory of integers with addition (Presburger arithmetic) and related theories; it introduces the method of Ehrenfeucht games. Chapter 3 deals with the theories of algebraically closed and real closed fields; the latter is one of the most famous examples of a decidable logical theory, and many algorithm have been developed in the past. Chapter 4 shows how the decidability of the theory of some class of algebraic structures carries over to cartesian products and generalized products of such structures; this is used to show the decidability of the theory of abelian groups. In the final chapter 5 the decidability of the theory of Boolean algebras and of linear orderings are shown.

Literature:

Lecture notes will be handed out.