Primitive recursive arithmetic: Difference between revisions

Revision as of 12:06, 2 October 2023

Revision as of 08:18, 3 October 2023

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 [[Finitism|finitisticfinitist]]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)|&epsilon;₀]],{{sfn|Kreisel|1960}} which is the [[Ordinal analysis#Definition|proof-theoretic ordinal]] of [[Peano arithmetic]]. PRA's proof theoretic ordinal is ω^ω, where ω is the smallest [[transfinite number|transfinite ordinal]]. PRA is sometimes called '''[[Skolem arithmetic]]'''.

The language of PRA can express arithmetic propositions involving [[natural number|natural numbers]]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 [[Metamathematics|metamathematicalmetamathematic]]al [[formal system]] for [[proof theory]], in particular for [[Consistency|consistency proofsproof]]s such as [[Gentzen's consistency proof]] of [[List of first-order theories#Arithmetic|first-order arithmetic]].

== Language and axioms ==

The language of PRA consists of:

* A [[Countable set|countably infinite]] number of variables ''x'', ''y'', ''z'',....

*The [[propositional calculus|propositional]] [[Logical connective|connectives]];

*The equality symbol ''='', the constant symbol 0, and the [[primitive recursive function|successor]] symbol ''S'' (meaning ''add one'');