Presburger Arithmetic & Other Fragments of Number Theory

Abstract

This work studies the decidability of different simplified versions of the firstorder theory of natural numbers, focusing on languages that include the successor function, the order relation, and addition. It begins by introducing the key concepts of first-order logic needed to understand the problem. Then, it looks at the natural numbers with just the successor function, and next with the addition of the order relation, showing that both of these theories are decidable using a technique called quantifier elimination. The work concludes with a proof of Presburger’s theorem, which proves that the first-order theory of natural numbers with addition, order, and successor is also decidable.