Peano Corto and Peano Basso: A Study of Local Induction in the Context of Weak Theories
Author:
Open Access
- 8 February 2014
- journal article
- research article
- Published by Wiley in Mathematical Logic Quarterly
- Vol. 60 (1-2) , 92-117
Abstract
In this paper we study local induction w.r.t. Σ1‐formulas over the weak arithmetic . The local induction scheme, which was introduced in , says roughly this: for any virtual class that is progressive, i.e., is closed under zero and successor, and for any non‐empty virtual class that is definable by a Σ1‐formula without parameters, the intersection of and is non‐empty. In other words, we have, for all Σ1‐sentences S, that S implies , whenever is progressive. Since, in the weak context, we have (at least) two definitions of Σ1, we obtain two minimal theories of local induction w.r.t. Σ1‐formulas, which we call Peano Corto and Peano Basso.In the paper we give careful definitions of Peano Corto and Peano Basso. We establish their naturalness both by giving a model theoretic characterization and by providing an equivalent formulation in terms of a sentential reflection scheme.The theories Peano Corto and Peano Basso occupy a salient place among the sequential theories on the boundary between weak and strong theories. They bring together a powerful collection of principles that is locally interpretable in . Moreover, they have an important role as examples of various phenomena in the metamathematics of arithmetical (and, more generally, sequential) theories. We illustrate this by studying their behavior w.r.t. interpretability, model interpretability and local interpretability. In many ways the theories are more like Peano arithmetic or Zermelo Fraenkel set theory, than like finitely axiomatized theories as Elementary Arithmetic, and . On the one hand, Peano Corto and Peano Basso are very weak: they are locally cut‐interpretable in . On the other hand, they behave as if they were strong: they are not contained in any consistent finitely axiomatized arithmetical theory, however strong. Moreover, they extend , the theory of parameter‐free Π1‐induction.Keywords
This publication has 30 references indexed in Scilit:
- A note on parameter free Π1-induction and restricted exponentiationMathematical Logic Quarterly, 2011
- HUME’S PRINCIPLE, BEGINNINGSThe Review of Symbolic Logic, 2011
- Can We Make the Second Incompleteness Theorem Coordinate Free?Journal of Logic and Computation, 2009
- Decidability of the theory of the natural integers with the cantor pairing function and the successorTheoretical Computer Science, 2001
- The unprovability of small inconsistencyArchive for Mathematical Logic, 1993
- An inside view of EXP; or, The closed fragment of the provability logic of IΔ0 + Ω1 with a prepositional constant for EXPThe Journal of Symbolic Logic, 1992
- A note on proofs of falsehoodArchive for Mathematical Logic, 1987
- On the scheme of induction for bounded arithmetic formulasAnnals of Pure and Applied Logic, 1987
- Cuts, consistency statements and interpretationsThe Journal of Symbolic Logic, 1985
- Axiomatizability by a schemaThe Journal of Symbolic Logic, 1968