People have always been fascinated by natural numbers, which are intuitively understood. In the late 19th century, mathematicians like Grassmann, Frege, and Dedekind provided formal definitions, leading to the development of axiomatic schemes that fundamentally shaped the logical understanding of mathematics. There has been a long-standing need for a comprehensive work on the metamathematics of first-order arithmetic. The authors aim to explore significant results in the study of Peano arithmetic and its subtheories. Although this field is vibrant, only a fraction of the findings have been documented in monographs. The book is organized into three parts: Part A develops mathematical and logical concepts across various fragments; Part B focuses on incompleteness; and Part C examines systems with the induction schema limited to bounded formulas, highlighting the connection between provability and computational complexity. Understanding formal systems for arithmetic is essential for grasping key results like Gödel's theorems. This work is designed for readers interested in deepening their knowledge of these systems and staying abreast of current research. It also includes an extensive bibliography of about 1000 items.
