Fragments of arithmetic (Q762484): Difference between revisions

The weakest system considered in this paper is the primitive recursive arithmetic (PRA) of Hilbert-Bernays, and the strongest are subsystems of analysis close to those considered by H. Friedman and by Minc. For instance (F) is the system whose axioms are quantifier free induction axioms (QF-IA) [but possibly with second order parameters in defining equations and in IA], (\(\exists f) f(x)=t[a/x]\) for every term t(a), \(\Sigma^ 0_ 1\)-IA, \(\Sigma^ 0_ 1\)-AC\({}_ 0\) \((=axioms\) of choice for numbers), and König's lemma for binary trees. This (F) is know to be strong enough for ordinary mathematics - for example, the Heine-Borel theorem and Gödels completeness theorem can be proved in it. And yet, the author's main result shows that (F) is conservative over (PRA). Also, there is a big bulk of results comparing \(\Pi^ 0_{n+1}\)- X and \(\Sigma^ 0_{m+1}\)-Y were X and Y are IA, the induction rule (IR), AC, comprehension axioms, etc. For instance, \(\Sigma^ 0_{n+1}\)- IA is strictly stronger than \(\Sigma^ 0_{n+1}\)-IR, and is equivalent to \(\Pi^ 0_{n+1}\)-IA. Although a substantial portion of these results are known (of course, the author makes refinements and improvements), what is to be noticed is that they are all proved by finitary proof theoretic means, like cut elimination and Herbrand expansions. (And so, no model theory, no indicators, and no ''Dialectica interpretation''). Also, operator theories \(OT_ n\) (i.e. theories with the \(\epsilon\)- symbol) are skillfully used by controlling subordination depths to n. If the situation is known when n is 0 or 1 in the original theory, the same can be done for \(OT_ n\); and then it translates back to \(n+1\) in the original setting.