Primitive recursive arithmetic: Difference between revisions

Revision as of 13:03, 12 July 2023

Latest revision as of 23:13, 6 July 2025

(24 intermediate revisions by 11 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|finitistic]]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)}}; however, Feferman calls this extension "no longer clearly finitary".</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 56:

</math>

Thus, the equations ''x''=''y'' and <math>|x - y| = 0</math> are equivalent. Therefore, the equations <math>|x - y| + |u - v| = 0</math> and <math>|x - y| \cdot |u - v| = 0</math> express the logical [[Logical conjunction|conjunction]] and [[disjunction]], respectively, of the equations ''x''=''y'' and ''u''=''v''. [[Negation]] can be expressed as <math>1 \dot - |x - y| = 0</math>.

== See also ==

Line 99:

|volume= 2

|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 120 ⟶ 109:

|contribution= Ordinal logics and the characterization of informal concepts of proof

|contribution-url = http://www.mathunion.org/ICM/ICM1958/Main/icm1958.0289.0299.ocr.pdf

|archive-url=https://web.archive.org/web/20170510093701/http://www.mathunion.org/ICM/ICM1958/Main/icm1958.0289.0299.ocr.pdf

|archive-date=10 May 2017

|___location= New York

|mr= 0124194

Line 140 ⟶ 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

|first= W.William W.

|authorlink= William W. Tait

|year= 1981

Line 155 ⟶ 158:

}}

*{{cite book

;Additional reading

|last= Tait

*{{cite journal

|first= William W.

|authorlink= William W. Tait

|date= June 2012

|chapter= Primitive Recursive Arithmetic and its Role in the Foundations of Arithmetic: Historical and Philosophical Reflections

|title= Epistemology versus Ontology

|pages= 302–333161–180

|chapter-url=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

}}

*{{cite journalbook

|last= Feferman

|first= Solomon

|author-link= Solomon Feferman

|year= 19931998

|titlechapter= What rests on what? The proof-theoretic analysis of mathematics

|chapter-url=https://math.stanford.edu/~feferman/papers/whatrests.pdf

|doi=10.1093/oso/9780195080308.003.0010

|journal= [[Philosophy of Mathematics]]

|title=In The Light Of Logic

|publisher= J. Czermak (ed.)

|pages= 1–147

}}

;===Additional reading===

*{{cite journal

|last= Rose