Primitive recursive arithmetic: Difference between revisions

Revision as of 12:06, 2 October 2023

Latest revision as of 23:13, 6 July 2025

(19 intermediate revisions by 8 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 [[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]].<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|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'');

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 121 ⟶ 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 141 ⟶ 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 163 ⟶ 165:

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

|title= Epistemology versus Ontology

|pages=161-180161–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 book

;Additional reading

*{{cite journal

|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