What can be done with PRA? Export

@article{citeulike:3758736, abstract = {Let S+ denote system JR?°2 + AC°1 in a classical second-order arithmetic, in which the induction rule is permitted to apply only to quantifier-free formulas and to ?°2 -formulas not containing functional variables, while the convolution axiom is permitted to apply only to ?°1 -formulas without functional variables. Also postulated is the closedness of the function class being examined, relative to primitive recursive operations. System, S+ turns out to be sufficiently rich: in it a theory of recursions and an elementary recursive analysis can be developed, a theorem on the continuity of effective operators and a theorem on cuteliminability from ? -deductions can be proved, and the usual analytic proofs of many number-theoretic theorems, including the prime distribution law, can be derived (with insignificant changes). (A formalization in S+ of the proof of Konig's lemma on paths in binary trees and of Godel's completeness theorem is described in the note.) On the other hand, the system admits of an interpretation in primitive recursive arithmetic (PRA). In particular, quantifier-free theorems in S+ are deducible in PRA, while theorems of form ?x?yR(x,y) with a quantifier-free formula R have calculi R (x,?(x)) with primitive recursive function ?, deducible in PRA. Thus, the suppressing part of operating constructive analysis can be developed already at the finite stages of the Shanin majorant hierarchy. In addition, a purely mechanical method exists for obtaining elementary number-theoretic proofs from many analytic proofs.}, author = {Mints, G. E.}, citeulike-article-id = {3758736}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/BF01693981}, citeulike-linkout-1 = {http://www.springerlink.com/content/gx79817466760203}, citeulike-linkout-2 = {http://www.zentralblatt-math.org/zmath/en/search/?q=an:0372.02018&format=complete}, citeulike-linkout-3 = {http://www.ams.org/mathscinet-getitem?mr=536652}, citeulike-linkout-4 = {http://www.zentralblatt-math.org/zmath/en/search/?q=an:0449.03055&format=complete}, day = {1}, doi = {10.1007/BF01693981}, journal = {Journal of Mathematical Sciences}, keywords = {\_copy, \_dipl, arithmetic, pra}, month = {November}, number = {5}, pages = {1487--1492}, posted-at = {2008-12-09 10:01:45}, priority = {0}, title = {What can be done with PRA?}, url = {http://dx.doi.org/10.1007/BF01693981}, volume = {14}, year = {1980} }

TY - JOUR ID - citeulike:3758736 L3 - citeulike-article-id:3758736 N2 - Let S+ denote system JR?°2 + AC°1 in a classical second-order arithmetic, in which the induction rule is permitted to apply only to quantifier-free formulas and to ?°2 -formulas not containing functional variables, while the convolution axiom is permitted to apply only to ?°1 -formulas without functional variables. Also postulated is the closedness of the function class being examined, relative to primitive recursive operations. System, S+ turns out to be sufficiently rich: in it a theory of recursions and an elementary recursive analysis can be developed, a theorem on the continuity of effective operators and a theorem on cuteliminability from ? -deductions can be proved, and the usual analytic proofs of many number-theoretic theorems, including the prime distribution law, can be derived (with insignificant changes). (A formalization in S+ of the proof of Konig's lemma on paths in binary trees and of Godel's completeness theorem is described in the note.) On the other hand, the system admits of an interpretation in primitive recursive arithmetic (PRA). In particular, quantifier-free theorems in S+ are deducible in PRA, while theorems of form ?x?yR(x,y) with a quantifier-free formula R have calculi R (x,?(x)) with primitive recursive function ?, deducible in PRA. Thus, the suppressing part of operating constructive analysis can be developed already at the finite stages of the Shanin majorant hierarchy. In addition, a purely mechanical method exists for obtaining elementary number-theoretic proofs from many analytic proofs. IS - 5 JF - Journal of Mathematical Sciences EP - 1492 TI - What can be done with PRA? VL - 14 SP - 1487 KW - _copy KW - _dipl KW - arithmetic KW - pra AU - Mints, GE PY - 1980/11/01/ UR - http://dx.doi.org/10.1007/BF01693981 ER -