Primitive recursive arithmetic: Difference between revisions

Revision as of 13:02, 10 November 2017

Latest revision as of 23:13, 6 July 2025

(40 intermediate revisions by 21 users not shown)

Line 1:

{{short description|Formalization of the natural numbers}}

'''Primitive recursive arithmetic''', or '''PRA''', is a [[Quantification (logic)|quantifier]]-free formalization of the [[natural numbers]]. It was first proposed by [[Thoralf Skolem|Skolem]]<ref>{{citation|first=Thoralf|last=Skolem|authorlink=Thoralf Skolem|year=1923|title=Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit unendlichem Ausdehnungsbereich|trans-title=The foundations of elementary arithmetic established by means of the recursive mode of thought without the use of apparent variables ranging over infinite domains|language=German|url=https://www.ucalgary.ca/rzach/files/rzach/skolem1923.pdf|journal=Skrifter utgit av Videnskapsselskapet i Kristiania. I, Matematisk-naturvidenskabelig klasse|volume=6|pages=1–38}}. Reprinted in translation in {{citation

| last = van Heijenoort | first = Jean | author-link = Jean van Heijenoort

'''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)}}; 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]].

| ___location = Cambridge, Mass.

| mr = 0209111

| pages = 302–333

| publisher = Harvard University Press

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

| year = 1967}}.</ref> as a formalization of his [[finitist]] conception of the [[foundations of mathematics|foundations of arithmetic]], and it is widely agreed that all reasoning of PRA is finitist. Many also believe that all of finitism is captured by PRA,<ref>{{citation|authorlink=William W. Tait|last=Tait|first= W.W.|year=1981|title=Finitism|journal=[[The Journal of Philosophy]]|volume=78|pages=524–546|doi=10.2307/2026089}}.</ref> but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to [[epsilon zero (mathematics)|&epsilon;₀]],<ref>{{citation

| last = Kreisel | first = G. | author-link = Georg Kreisel

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

| ___location = New York

| mr = 0124194

| pages = 289–299

| publisher = Cambridge University Press

| title = Proceedings of the International Congress of Mathematicians, 1958

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

| year = 1960}}.</ref> which is the [[proof-theoretic ordinal]] of [[Peano arithmetic]]. PRA's proof theoretic ordinal is ω^ω, where ω is the smallest transfinite ordinal. PRA is sometimes called '''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 22 ⟶ 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 29 ⟶ 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:

Further, 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 47 ⟶ 35:

In [[first-order arithmetic]], the only [[primitive recursive function]]s that need to be explicitly axiomatized are [[addition]] and [[multiplication]]. All other primitive recursive predicates can be defined using these two primitive recursive functions and [[Quantification (logic)|quantification]] over all [[natural numbers]]. Defining [[primitive recursive function]]s in this manner is not possible in PRA, because it lacks quantifiers.

−== Logic-free calculus ==

It is possible to formalise PRA in such a way that it has no logical connectives at all—a sentence of PRA is just an equation between two terms. In this setting a term is a primitive recursive function of zero or more variables. In {{harvtxt|Curry|1941 [[Haskell Curry]]}} gave the first such system.<ref> The rule of induction in Curry's system was unusual. A later refinement was given by {{citationharvtxt|Goodstein|1954}}. The [[Rule of inference|rule]] of induction in Goodstein's system is:

| last = Curry | first = Haskell B. | author-link = Haskell Curry

| doi = 10.2307/2371522

| journal = [[American Journal of Mathematics]]

| mr = 0004207

| pages = 263–282

| title = A formalization of recursive arithmetic

| volume = 63

| year = 1941}}.</ref> The rule of induction in Curry's system was unusual. A later refinement was given by [[Reuben Goodstein]].<ref>{{citation

| last = Goodstein | first = R. L. | author-link = Reuben Goodstein

| journal = Mathematica Scandinavica

| mr = 0087614

| pages = 247–261

| title = Logic-free formalisations of recursive arithmetic

| volume = 2

| year = 1954}}.</ref> The [[Rule of inference|rule]] of induction in Goodstein's system is:

:<math>{F(0) = G(0) \quad F(S(x)) = H(x,F(x)) \quad G(S(x)) = H(x,G(x)) \over F(x) = G(x)}.</math>

Line 83 ⟶ 56:

</math>

Thus, the equations x=y and |''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 ==

* [[Elementary recursive arithmetic]]

* [[Finite-valued logic]]

* [[Heyting arithmetic]]

* [[Peano arithmetic]]

* [[Second-order arithmetic]]

* [[Primitive recursive function]]

* [[Robinson arithmetic]]

* [[Second-order arithmetic]]

* [[Skolem arithmetic]]

==ReferencesNotes==

<references/>

==References==

;Additional reading

*{{citation

*{{cite journal

| last = Rose | first = H. E.

|last= Curry

| journal = Zeitschrift für Mathematische Logik und Grundlagen der Mathematik

|first= Haskell B.

| mr = 0140413

|author-link= Haskell Curry

| pages = 124–135

|year= 1941

| title = On the consistency and undecidability of recursive arithmetic

|title= A formalization of recursive arithmetic

| volume = 7

|journal= [[American Journal of Mathematics]]

| year = 1961}}.

|mr= 0004207

|pages= 263–282

|volume= 63

|issue= 2

|doi= 10.2307/2371522

|jstor= 2371522

}}

*{{cite journal

|last= Goodstein

|first= R. L.

|author-link= Reuben Goodstein

|year= 1954

|title= Logic-free formalisations of recursive arithmetic

|journal= Mathematica Scandinavica

|mr= 0087614

|pages= 247–261

|volume= 2

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

|doi-access= free

}}

*{{Cite conference

|last= Kreisel

|first= Georg

|author-link= Georg Kreisel

|year= 1960

|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

|pages= 289–299

|publisher= Cambridge University Press

|title= Proceedings of the International Congress of Mathematicians, 1958

}}

*{{cite journal

|last= Skolem

|first= Thoralf

|authorlink= Thoralf Skolem

|year= 1923

|title= Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit unendlichem Ausdehnungsbereich

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

|language= German

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

|journal= Skrifter Utgit av Videnskapsselskapet I Kristiania. I, Matematisk-naturvidenskabelig Klasse

|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

|editor-link=Jean van Heijenoort

|pages=302–333

|last=Skolem

|first=Thoralf

|mr=0209111

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

*{{cite journal

|last= Tait

|first= William W.

|authorlink= William W. Tait

|year= 1981

|title= Finitism

|journal= [[The Journal of Philosophy]]

|volume= 78

|issue= 9

|pages= 524–546

|doi= 10.2307/2026089

|jstor= 2026089

}}

*{{cite book

|last= Tait

|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=161–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

|last= Feferman

|first= Solomon

|author-link= Solomon Feferman

|year=1998

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

|title=In The Light Of Logic

}}

===Additional reading===

*{{cite journal

|last= Rose

|first= H. E.

|year= 1961

|title= On the consistency and undecidability of recursive arithmetic

|journal= Zeitschrift für Mathematische Logik und Grundlagen der Mathematik

|mr= 0140413

|pages= 124–135

|volume= 7

|issue= 7–10

|doi= 10.1002/malq.19610070707

}}

{{Mathematical logic}}

* [[Solomon Feferman|Feferman, S]] (1992) ''[https://math.stanford.edu/~feferman/papers/whatrests.pdf What rests on what? The proof-theoretic analysis of mathematics]''. Invited lecture, 15th int'l Wittgenstein symposium.

[[Category:Constructivism (mathematics)]]