Primitive recursive arithmetic: Difference between revisions

Revision as of 22:32, 24 August 2022

Latest revision as of 23:13, 6 July 2025

(31 intermediate revisions by 15 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 finitistfinitistic. 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 8:

The language of PRA consists of:

* A [[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'');

*A symbol for each [[primitive recursive function]].

Line 15:

* [[tautology (logic)|Tautologies]] of the [[propositional calculus]];

* Usual axiomatization of [[Equality (mathematics)|equality]] as an [[equivalence relation]].

The logical rules of PRA are [[modus ponens]] and [[First-order logic#SubstitutionRules of inference|variable substitution]].<br>

The non-logical axioms are, firstly:

* <math>S(x) \neneq 0</math>;

* <math>S(x)=S(y) ~\to~ x = y,</math>

where <math>x \neq y</math> always denotes the negation of <math>x = y</math> so that, for example, <math>S(0) = 0</math> is a negated proposition.

and recursive defining equations for every [[primitive recursive function]] as desired. For instance, the most common characterization of the primitive recursive functions is as the 0 constant and successor function closed under projection, composition and primitive recursion. So for a (''n''+1)-place function ''f'' defined by primitive recursion over a ''n''-place base function ''g'' and (''n''+2)-place iteration function ''h'' there would be the defining equations:

andFurther, recursive defining equations for every [[primitive recursive function]] may be adopted as axioms as desired. For instance, the most common characterization of the primitive recursive functions is as the 0 constant and successor function closed under projection, composition and primitive recursion. So for a (''n''+1)-place function ''f'' defined by primitive recursion over a ''n''-place base function ''g'' and (''n''+2)-place iteration function ''h'' there would be the defining equations:

* <math>f(0,y_1,\ldots,y_n) = g(y_1,\ldots,y_n)</math>

* <math>f(S(x),y_1,\ldots,y_n) = h(x,f(x,y_1,\ldots,y_n),y_1,\ldots,y_n)</math>

Line 54 ⟶ 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 81 ⟶ 83:

|pages= 263–282

|volume= 63

|issue= 2

|doi= 10.2307/2371522

|jstor= 2371522

}}

Line 94 ⟶ 98:

|pages= 247–261

|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 115 ⟶ 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 131 ⟶ 127:

|language= German

|url= https://www.ucalgary.ca/rzach/files/rzach/skolem1923.pdf

|journal= Skrifter utgitUtgit av Videnskapsselskapet iI Kristiania. I, Matematisk-naturvidenskabelig klasseKlasse

|volume= 6

|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 144 ⟶ 152:

|journal= [[The Journal of Philosophy]]

|volume= 78

|issue= 9

|pages= 524–546

|doi= 10.2307/2026089

|jstor= 2026089

}}

*{{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

Line 170 ⟶ 193:

|pages= 124–135

|volume= 7

|issue= 7–10

|doi= 10.1002/malq.19610070707

}}