Primitive recursive arithmetic: Difference between revisions

Revision as of 23:00, 22 February 2012

Revision as of 17:06, 12 October 2012

Line 1:

'''Primitive recursive arithmetic''', or '''PRA''', is a [[quantifier]]-free formalization of the [[natural numbers]]. It was first proposed by [[Thoralf Skolem|Skolem]]<ref>[[Thoralf Skolem]] (1923) "The foundations of elementary arithmetic" in [[Jean van Heijenoort]], translator and ed. (1967) ''From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931''. Harvard Univ. Press: 302-33.</ref> as a formalization of his [[finitist]] conception of the [[foundations of mathematics|foundations of arithmetic]], and it is widely agreed that all reasoning of PRA is finitist. Many also believe that all of finitism is captured by PRA,<ref>[[William W. Tait|Tait, W.W.]] (1981), "Finitism", ''Journal of Philosophy'' 78:524-46.</ref>, but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to [[epsilon 0|&epsilon;₀]],<ref>[[Georg Kreisel]] (1958) "Ordinal Logics and the Characterization of Informal Notions of Proof," ''Proc. Internat. Cong. Mathematicians'': 289-99.</ref>, which is the [[proof-theoretic ordinal]] of [[Peano arithmetic]]. PRA's proof theoretic ordinal is &omega;ω^&omega;ω, where &omega;ω is the smallest transfinite ordinal. PRA is sometimes called '''Skolem arithmetic'''.

The language of PRA can express arithmetic propositions involving [[natural number]]s and any [[primitive recursive function]], including the operations of [[addition]], [[multiplication]], and [[exponentiation]]. PRA cannot explicitly quantify over the ___domain of natural numbers. PRA is often taken as the basic [[metamathematic]]al [[formal system]] for [[proof theory]], in particular for [[consistency proof]]s such as [[Gentzen's consistency proof]] of [[first-order arithmetic]].

Line 29:

== Logic-free calculus ==

It is possible to formalise PRA in such a way that it has no logical connectives at all - a sentence of PRA is just an equation between two terms. In this setting a term is a primitive recursive function of zero or more variables. In 1941 [[Haskell Curry]] gave the first such system.<ref>[[Haskell Curry]], ''[http://www.jstor.org/stable/2371522 A Formalization of Recursive Arithmetic]''. [[American Journal of Mathematics]], vol 63 no 2 (1941) pp 263-282</ref>. The rule of induction in Curry's system was unusual. A later refinement was given by [[Reuben Goodstein]].<ref>[[Reuben Goodstein]], ''[http://www.digizeitschriften.de/resolveppn/GDZPPN002343355 Logic-free formalisations of recursive arithmetic]'', [[Mathematica Scandinavica]] vol 2 (1954) pp 247-261</ref>. The rule of induction in Goodstein's system is:

<math>{F(0) = G(0) \quad F(S(x)) = H(x,F(x)) \quad G(S(x)) = H(x,G(x)) \over F(x) = G(x)}.</math>