## Decidable Logical Theories

Dr. Heinrich Rolletschek

September 11, 2018

### Time and place:

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

### 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:

This course deals with one important aspect of automated theorem proving. Let K
be some class of algebraic structures (models), for instance, the class of all groups or
linear orderings, or the class consisting only of the field of real numbers. The question
arises if there exists an algorithm for deciding whether or not a given sentence ϕ
belongs to the theory of K, that is, whether or not ϕ is satisfied by every model
in K. The answer is negative in general, but in several cases of interest a decision
algorithm does indeed exist and will be developed in the lecture. A number of
general techniques will be introduced, the most important being quantifier
elimination.

### Course contents:

Chapter 1 uses some very simple logical theories to illustrate the basic method of
quantifier elimination, as well as model-theoretic methods for proving decidability.
Chapter 2 deals with the theory of integers with addition (Presburger arithmetic)
and related theories; it introduces the general 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 a decidability result for some class of algebraic structures carries
over to cartesian products and generalized products; this allows to show
the decidability of the theory of abelian groups. In the final Chapter 5 the
decidability of the theories of Boolean algebras and of linear orderings are
shown.

### Literature:

Lecture notes will be handed out.