Peano’s smart children: A provability logical study of systems with built-in consistency

The systems studied in this article prove the same theorems (from the “extensional” point of view) as Peano Arithmetic, but are equipped with a self-correction procedure. These systems prove their own consistency and thus escape Godel’s second theorem. Here, the provability logics of these systems are studied. An application of the results obtained turns out to be the solution to a problem of Orey on relative interpretability.