Primitive recursive arithmetic: Difference between revisions

Revision as of 03:59, 20 January 2017

Latest revision as of 23:13, 6 July 2025

(44 intermediate revisions by 25 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 apparrent 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, even though it is also widely agreed that the reasoning of PRA is not ultrafinitist. 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 48 ⟶ 36:

== Logic-free calculus ==

It is possible to formalise PRA in such a way that it has no logical connectives at all - aall—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 78 ⟶ 51:

\begin{align}

P(0) = 0 \quad & \quad P(S(x)) = x \\

x \dot - 0 = x \quad & \quad x \mathrel{\dot -} S(y) = P(x \mathrel{\dot -} y) \\

|x - y| = & (x \mathrel{\dot -} y) + (y \mathrel{\dot -} x). \\

\end{align}

</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)]]