Peano Basso and Peano Corto

Abstract

In this paper we show that the theories Peano Corto (or: PA↓↓ := I(Σ∞, Σ1,0)) and Peano Basso (or: PA↓ := I(Σ∞, Σ1,1)), two theories of local induction, are locally cut-interpretable in the basic arithmetic PA−. We prove a number of theorems about Peano Corto and Peano Basso. We provide some insights that illustrate that these theories are in many respects analogues of full Peano Arithmetic PA. The theory PA↓↓ extends the theory of parameter-free Π1-induction, IΠ−1 . Hence, IΠ−1 is locally cut-interpretable in PA−. We will draw a number of consequences of this fact for IΠ−1.