Content deleted Content added
Toby Bartels (talk | contribs) Clarify that Skolem arithmetic covers something different. |
→top: per WP:EASTEREGG |
||
Line 1:
{{short description|Formalization of the natural numbers}}
'''Primitive recursive arithmetic''' ('''PRA''') is a [[Quantification (logic)|quantifier]]-free formalization of the [[natural numbers]]. It was first proposed by Norwegian mathematician {{harvtxt|Skolem|1923}},<ref>reprinted in translation in {{harvtxt|van Heijenoort|1967}}</ref> as a formalization of his [[finitist]]ic conception of the [[foundations of mathematics|foundations of arithmetic]], and it is widely agreed that all reasoning of PRA is finitistic. Many also believe that all of finitism is captured by PRA,{{sfn|Tait|1981}} but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to [[epsilon zero (mathematics)|ε<sub>0</sub>]],{{sfn|Kreisel|1960}} which is the [[proof-theoretic ordinal]] of [[Peano arithmetic]]. PRA's proof theoretic ordinal is ω<sup>ω</sup>, where ω is the smallest [[transfinite number|transfinite ordinal]]. PRA is sometimes called ''Skolem arithmetic'', although that has another meaning, see [[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]].
| |||