Primitive recursive arithmetic: Difference between revisions

Revision as of 05:53, 3 April 2022

Revision as of 10:44, 1 August 2022

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 [[Thoralf {{harvtxt|Skolem]]|1923}}, <ref>reprinted in translation in {{citationharvtxt|first=Thoralfvan Heijenoort|last=Skolem|authorlink=Thoralf1967}}</ref> Skolemas a formalization of his [[finitist]] conception of the [[foundations of mathematics|year=1923|title=Begründungfoundations derof elementarenarithmetic]], Arithmetikand durchit dieis rekurrierendewidely Denkweiseagreed ohnethat Anwendungall scheinbarerreasoning Veränderlichenof mitPRA unendlichemis Ausdehnungsbereich|trans-title=Thefinitist. foundationsMany also believe that all of elementaryfinitism arithmeticis establishedcaptured by meansPRA,{{sfn|Tait|1981}} ofbut theothers recursivebelieve modefinitism ofcan thoughtbe withoutextended theto useforms of apparentrecursion variablesbeyond rangingprimitive overrecursion, infiniteup domains|language=Germanto [[epsilon zero (mathematics)|url=https:&epsilon;<sub>0<//www.ucalgary.ca/rzach/files/rzach/skolem1923.pdfsub>]],{{sfn|journal=SkrifterKreisel|1960}} utgitwhich avis Videnskapsselskapetthe i[[proof-theoretic Kristianiaordinal]] of [[Peano arithmetic]]. I PRA's proof theoretic ordinal is ω^ω, Matematisk-naturvidenskabeligwhere klasse|volume=6ω is the smallest [[transfinite number|pages=1–38}}transfinite ordinal]]. Reprinted inPRA translationis insometimes {{citationcalled '''[[Skolem arithmetic]]'''.

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

| ___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 number|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 50 ⟶ 34:

== 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 89 ⟶ 58:

== See also ==

* [[Elementary recursive arithmetic]]

* [[Finite-valued logic]]

* [[Heyting arithmetic]]

* [[Peano arithmetic]]

* [[Second-order arithmetic]]

* [[Primitive recursive function]]

* [[Finite-valuedRobinson logicarithmetic]]

* [[Second-order arithmetic]]

* [[Skolem arithmetic]]

==ReferencesNotes==

<references/>

==References==

*{{cite journal

|last= Curry

|first= Haskell B.

|author-link= Haskell Curry

|year= 1941

|title= A formalization of recursive arithmetic

|journal= [[American Journal of Mathematics]]

|mr= 0004207

|pages= 263–282

|volume= 63

|doi= 10.2307/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

}}

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

}}

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

|___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 journal

|last= Tait

|first= W.W.

|authorlink= William W. Tait

|year= 1981

|title= Finitism

|journal= [[The Journal of Philosophy]]

|volume= 78

|pages= 524–546

|doi= 10.2307/2026089

}}

;Additional reading

*{{cite journal

*{{citation

| last = Rose | first = H. E.Feferman

|first= Solomon

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

|author-link= Solomon Feferman

| mr = 0140413

|year= 1993

| pages = 124–135

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

| title = On the consistency and undecidability of recursive arithmetic

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

| volume = 7

|journal= [[Philosophy of Mathematics]]

| year = 1961}}.

|publisher= J. Czermak (ed.)

|pages= 1–147

}}

*{{cite journal

* [[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.

|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

|doi= 10.1002/malq.19610070707

}}

[[Category:Constructivism (mathematics)]]