Primitive recursive arithmetic (PRA) is aquantifier-free formalization of thenatural numbers. It was first proposed by Norwegian mathematicianSkolem (1923),^[1] as a formalization of hisfinitistic conception of thefoundations 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,^[2] but others believe finitism can be extended to forms of recursion beyond primitive recursion, up toε₀,^[3] which is theproof-theoretic ordinal ofPeano arithmetic.^[4] PRA's proof theoretic ordinal is ω^ω, where ω is the smallesttransfinite ordinal. PRA is sometimes calledSkolem arithmetic, although that has another meaning, seeSkolem arithmetic.

The language of PRA can express arithmetic propositions involvingnatural numbers and anyprimitive recursive function, including the operations ofaddition,multiplication, andexponentiation. PRA cannot explicitly quantify over the domain of natural numbers. PRA is often taken as the basicmetamathematicalformal system forproof theory, in particular forconsistency proofs such asGentzen's consistency proof offirst-order arithmetic.

The language of PRA consists of:

• Acountably infinite number of variablesx,y,z,....
• Thepropositionalconnectives;
• The equality symbol=, the constant symbol 0, and thesuccessor symbolS (meaningadd one);
• A symbol for eachprimitive recursive function.

The logical axioms of PRA are the:

• Tautologies of thepropositional calculus;
• Usual axiomatization ofequality as anequivalence relation.

The logical rules of PRA aremodus ponens andvariable substitution.
The non-logical axioms are, firstly:

• ${\displaystyle S(x)\ne 0}$;
• ${\displaystyle S(x)=S(y)\to x=y,}$

where${\displaystyle x\ne y}$ always denotes the negation of${\displaystyle x=y}$ so that, for example,${\displaystyle S(0)=0}$ is a negated proposition.

Further, recursive defining equations for everyprimitive 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 functionf defined by primitive recursion over an-place base functiong and (n+2)-place iteration functionh there would be the defining equations:

• ${\displaystyle f(0,y_1,\dots ,y_n)=g(y_1,\dots ,y_n)}$
• ${\displaystyle f(S(x),y_1,\dots ,y_n)=h(x,f(x,y_1,\dots ,y_n),y_1,\dots ,y_n)}$

Especially:

• ${\displaystyle x+0=x}$
• ${\displaystyle x+S(y)=S(x+y)}$
• ${\displaystyle x\cdot 0=0}$
• ${\displaystyle x\cdot S(y)=x\cdot y+x}$
• ... and so on.

PRA replaces theaxiom schema of induction forfirst-order arithmetic with the rule of (quantifier-free) induction:

• From${\displaystyle \phi (0)}$ and${\displaystyle \phi (x)\to \phi (S(x))}$, deduce${\displaystyle \phi (y)}$, for any predicate${\displaystyle \phi .}$

Infirst-order arithmetic, the onlyprimitive recursive functions that need to be explicitly axiomatized areaddition andmultiplication. All other primitive recursive predicates can be defined using these two primitive recursive functions andquantification over allnatural numbers. Definingprimitive recursive functions in this manner is not possible in PRA, because it lacks quantifiers.

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.Curry (1941) gave the first such system. The rule of induction in Curry's system was unusual. A later refinement was given byGoodstein (1954). Therule of induction in Goodstein's system is:

${\displaystyle \frac{F(0)=G(0)F(S(x))=H(x,F(x))G(S(x))=H(x,G(x))}{F(x)=G(x)}.}$

Herex is a variable,S is the successor operation, andF,G, andH are any primitive recursive functions which may have parameters other than the ones shown. The only otherinference rules of Goodstein's system are substitution rules, as follows:

${\displaystyle \frac{F(x)=G(x)}{F(A)=G(A)}\frac{A=B}{F(A)=F(B)}\frac{A=BA=C}{B=C}.}$

HereA,B, andC are any terms (primitive recursive functions of zero or more variables). Finally, there are symbols for any primitive recursive functions with corresponding defining equations, as in Skolem's system above.

In this way the propositional calculus can be discarded entirely. Logical operators can be expressed entirely arithmetically, for instance, the absolute value of the difference of two numbers can be defined by primitive recursion:

Thus, the equationsx=y and${\displaystyle |x-y|=0}$ are equivalent. Therefore, the equations${\displaystyle |x-y|+|u-v|=0}$ and${\displaystyle |x-y|\cdot |u-v|=0}$ express the logicalconjunction anddisjunction, respectively, of the equationsx=y andu=v.Negation can be expressed as${\displaystyle 1\dot{-}|x-y|=0}$.

• Elementary recursive arithmetic
• Finite-valued logic
• Heyting arithmetic
• Peano arithmetic
• Primitive recursive function
• Robinson arithmetic
• Second-order arithmetic
• Skolem arithmetic

• Curry, Haskell B. (1941). "A formalization of recursive arithmetic".American Journal of Mathematics.63 (2):263–282.doi:10.2307/2371522.JSTOR 2371522.MR 0004207.

• Goodstein, R. L. (1954)."Logic-free formalisations of recursive arithmetic".Mathematica Scandinavica.2:247–261.doi:10.7146/math.scand.a-10412.MR 0087614.

• Kreisel, Georg (1960)."Ordinal logics and the characterization of informal concepts of proof"(PDF).Proceedings of the International Congress of Mathematicians, 1958. New York: Cambridge University Press. pp. 289–299.MR 0124194. Archived fromthe original(PDF) on 10 May 2017.

• Skolem, Thoralf (1923)."Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit unendlichem Ausdehnungsbereich" [The foundations of elementary arithmetic established by means of the recursive mode of thought without the use of apparent variables ranging over infinite domains](PDF).Skrifter Utgit av Videnskapsselskapet I Kristiania. I, Matematisk-naturvidenskabelig Klasse (in German).6:1–38.
  • Skolem, Thoralf (1967) [1923]. "The foundations of elementary arithmetic established by means of the recursive mode of thought, without the use of apparent variables ranging over infinite domains". Invan Heijenoort, Jean (ed.).From Frege to Gödel. Harvard University Press. pp. 302–333.MR 0209111.(accessible to patrons with print disabilities)
• Tait, William W. (1981). "Finitism".The Journal of Philosophy.78 (9):524–546.doi:10.2307/2026089.JSTOR 2026089.

• Tait, William W. (June 2012)."Primitive Recursive Arithmetic and its Role in the Foundations of Arithmetic: Historical and Philosophical Reflections"(PDF).Epistemology versus Ontology. pp. 161–180.doi:10.1007/978-94-007-4435-6_8. Archived fromthe original(PDF) on 24 May 2024.

• Feferman, Solomon (1998)."What rests on what? The proof-theoretic analysis of mathematics"(PDF).In The Light Of Logic.doi:10.1093/oso/9780195080308.003.0010.

• Rose, H. E. (1961). "On the consistency and undecidability of recursive arithmetic".Zeitschrift für Mathematische Logik und Grundlagen der Mathematik.7 (7–10):124–135.doi:10.1002/malq.19610070707.MR 0140413.

• Constructivism (philosophy of mathematics)
• Formal theories of arithmetic

• Articles with short description
• Short description is different from Wikidata
• CS1 German-language sources (de)
• Pages with references accessible to Internet Archive patrons with print disabilities