Primitive recursive arithmetic: Difference between revisions

Revision as of 21:16, 2 January 2025

Latest revision as of 23:13, 6 July 2025

(7 intermediate revisions by 4 users not shown)

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)|&epsilon;₀]],{{sfn|Kreisel|1960}} which is the [[proof-theoretic ordinal]] of [[Peano arithmetic]].<ref>{{harvtxt|Feferman|1998|p=4 (of personal website version)}}; Feferman differs from Kreisel's usage of 'finitism':{{clarify|date=January 2025|reason=Ishowever, Feferman critiquingcalls Kreisel'sthis usageextension directly, or are the contexts different?}}<blockquote>"The principle [of transfinite induction up to &epsilon;₀] may itself be justified on ''constructive'' grounds (though ''no longer clearly finitary grounds'', even for decidable predicates".)" (emphasis added)</blockquote></ref> PRA's proof theoretic ordinal is ω^ω, 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]].

Line 100:

|doi= 10.7146/math.scand.a-10412

|doi-access= free

}}

*{{cite book

|last= van Heijenoort

|first= Jean

|author-link= Jean van Heijenoort

|year= 1967

|title= From Frege to Gödel. A source book in mathematical logic, 1879–1931

|___location= Cambridge, Mass.

|mr= 0209111

|pages= 302–333

|publisher= Harvard University Press

}}

Line 143 ⟶ 131:

|pages= 1–38

}}

**{{cite book

|chapter=The foundations of elementary arithmetic established by means of the recursive mode of thought, without the use of apparent variables ranging over infinite domains

|title=From Frege to Gödel

|year= 1967

|orig-year=1923

|editor-first=Jean

|editor-last= van Heijenoort

|authoreditor-link= Jean van Heijenoort

|pages=302–333

|last=Skolem

|first= JeanThoralf

|mr= 0209111

|publisher=Harvard University Press|ref=CITEREFvan_Heijenoort1967}} {{IAp|https://archive.org/details/fromfregetogodel0025unse/page/302/mode/2up}}

*{{cite journal

|last= Tait

Line 166:

|title= Epistemology versus Ontology

|pages=161–180

|chapter-url=https://web.archive.org/web/20240524221357/https://home.uchicago.edu/~wwtx/PRA2.pdf

|doi=10.1007/978-94-007-4435-6_8

|archive-url= https://web.archive.org/web/20240524221357/https://home.uchicago.edu/~wwtx/PRA2.pdf

|archive-date= 24 May 2024

}}