PEANO ARITHMETIC AND ITS SUBSYSTEMS

Peano Arithmetic is the first order theory of ℕ with simple axioms for +, ·, ≤, and the induction axiom scheme. Here we focus on the subsystem I Δ 0 of Peano Arithmetic, in which induction is restricted to bounded formulas. This subsystem plays an essential role in the development of the theories in later chapters: All (two-sorted) theories introduced in this book extend V 0 , which is a conservative extension of I Δ 0 . At the end of the chapter we briefly discuss Buss's hierarchy. These single-sorted theories establish a link between bounded arithmetic and the polynomial time hierarchy, and have played a central role in the study of bounded arithmetic. In later chapters we introduce their twosorted versions, including V 1 , a theory that characterizes P . The theories considered in this chapter are singled-sorted, and the intended domain is ℕ = {0, 1, 2, …}. Subsection III.3.3 shows that the relation y = 2 x is definable by a bounded formula in the vocabulary of I Δ 0 , and in Section III.4 this is used to show that bounded formulas represent precisely the relations in the Linear Time Hierarchy ( LTH ). Peano Arithmetic See Section II.2 for notions such as vocabulary, formula , and logical consequence . Definition III.1.1. A theory over a vocabulary L is a set T of formulas over L which is closed under logical consequence and universal closure.