Decidability of Presburger arithmetic

Decidability of Presburger arithmetic Vincent Thomas 16th January 2006 Contents 1 Decidability 1 2 Presburger arithmetic 2 2.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Early results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.3 Elimination of quantifiers . . . . . . . . . . . . . . . . . . . . . . 3 Introduction When given a theory, an important question is to know if it is decidable. The famous theorem of Godel shows in many cases, it is not. But sometimes, we have a positive answer. It is precisely the case of Presburger arithmetic. In all what follows, we use the first order classic logic. 1 Decidability Definition 1 A theory T over a language L is called decidable if there is an algorithm which answers to the question : T F ? for any formula F over L. A theory T over a language L is called recursive if there is an algorithm which answers to the question : F ? T ? The main tool we will use to prove the wanted result is the elimination of quan- tifiers.

• induction over


• without quantifier


• called decidable


• f1 ?


• first result


• ?xf ?


• early results


• lemma hypothesis


• need