Primitive recursive arithmetic

Last updated January 05, 2025

Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Norwegian mathematician Skolem (1923),^[1] as a formalization of his finitistic conception of the 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,^[2] but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε₀,^[3] which is the proof-theoretic ordinal of Peano arithmetic.^[4] PRA's proof theoretic ordinal is ω^ω, where ω is the smallest 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 numbers 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 metamathematical formal system for proof theory, in particular for consistency proofs such as Gentzen's consistency proof of first-order arithmetic.

Language and axioms

The language of PRA consists of:

A countably infinite number of variables x, y, z,....
The propositional connectives;
The equality symbol =, the constant symbol 0, and the successor symbol S (meaning add one);
A symbol for each primitive recursive function.

The logical axioms of PRA are the:

Tautologies of the propositional calculus;
Usual axiomatization of equality as an equivalence relation.

The logical rules of PRA are modus ponens and variable substitution.
The non-logical axioms are, firstly:

$S(x)\neq 0$ ;
$S(x)=S(y)\to x=y,$

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

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:

$f(0,y_{1},\ldots ,y_{n})=g(y_{1},\ldots ,y_{n})$
$f(S(x),y_{1},\ldots ,y_{n})=h(x,f(x,y_{1},\ldots ,y_{n}),y_{1},\ldots ,y_{n})$

Especially:

$x+0=x\$
$x+S(y)=S(x+y)\$
$x\cdot 0=0\$
$x\cdot S(y)=x\cdot y+x\$
... and so on.

PRA replaces the axiom schema of induction for first-order arithmetic with the rule of (quantifier-free) induction:

From $\varphi (0)$ and $\varphi (x)\to \varphi (S(x))$ , deduce $\varphi (y)$ , for any predicate $\varphi .$

In first-order arithmetic, the only primitive recursive functions 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 over all natural numbers. Defining primitive recursive functions 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. Curry (1941) gave the first such system. The rule of induction in Curry's system was unusual. A later refinement was given by Goodstein (1954). The rule of induction in Goodstein's system is:

{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)}.

Here x is a variable, S is the successor operation, and F, G, and H are any primitive recursive functions which may have parameters other than the ones shown. The only other inference rules of Goodstein's system are substitution rules, as follows:

{F(x)=G(x) \over F(A)=G(A)}\qquad {A=B \over F(A)=F(B)}\qquad {A=B\quad A=C \over B=C}.

Here A, B, and C 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:

{\begin{aligned}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{aligned}}

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

Notes

↑ reprinted in translation in van Heijenoort (1967)
↑ Tait 1981.
↑ Kreisel 1960.
↑ Feferman (1998 , p. 4 (of personal website version)) Feferman differs from Kreisel's usage of 'finitism':^{[ clarification needed ]}
"The principle [of transfinite induction up to ε₀] may itself be justified on constructive grounds (though no longer clearly finitary grounds, even for decidable predicates.)" (emphasis added)

Related Research Articles

In computability theory, the Ackermann function, named after Wilhelm Ackermann, is one of the simplest and earliest-discovered examples of a total computable function that is not primitive recursive. All primitive recursive functions are total and computable, but the Ackermann function illustrates that not all total computable functions are primitive recursive.

First-order logic—also called predicate logic, predicate calculus, quantificational logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables. Rather than propositions such as "all men are mortal", in first-order logic one can have expressions in the form "for all x, if x is a man, then x is mortal"; where "for all x" is a quantifier, x is a variable, and "... is a man" and "... is mortal" are predicates. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 is not easy to read today; it uses concepts and formalisms that are no longer used and terminology that is often obscure. The version given below attempts to represent all the steps in the proof and all the important ideas faithfully, while restating the proof in the modern language of mathematical logic. This outline should not be considered a rigorous proof of the theorem.

The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. Sometimes, it is called first-order propositional logic to contrast it with System F, but it should not be confused with first-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, biconditional, and negation. Some sources include other connectives, as in the table below.

In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops. Primitive recursive functions form a strict subset of those general recursive functions that are also total functions.

In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th-century Italian mathematician Giuseppe Peano. These axioms have been used nearly unchanged in a number of metamathematical investigations, including research into fundamental questions of whether number theory is consistent and complete.

In mathematical logic and computer science, a general recursive function, partial recursive function, or μ-recursive function is a partial function from natural numbers to natural numbers that is "computable" in an intuitive sense – as well as in a formal one. If the function is total, it is also called a total recursive function. In computability theory, it is shown that the μ-recursive functions are precisely the functions that can be computed by Turing machines. The μ-recursive functions are closely related to primitive recursive functions, and their inductive definition (below) builds upon that of the primitive recursive functions. However, not every total recursive function is a primitive recursive function—the most famous example is the Ackermann function.

In classical, deductive logic, a consistent theory is one that does not lead to a logical contradiction. A theory $is consistent if there is no formula such that both and its negation are elements of the set of consequences of . Let be a set of closed sentences and the set of closed sentences provable from under some formal deductive system. The set of axioms is consistent when there is no formula such that and . A trivial theory is clearly inconsistent. Conversely, in an explosive formal system every inconsistent theory is trivial. Consistency of a theory is a syntactic notion, whose semantic counterpart is satisfiability. A theory is satisfiable if it has a model, i.e., there exists an interpretation under which all axioms in the theory are true. This is what consistent meant in traditional Aristotelian logic, although in contemporary mathematical logic the term satisfiable is used instead.$

In computability theory, Kleene's recursion theorems are a pair of fundamental results about the application of computable functions to their own descriptions. The theorems were first proved by Stephen Kleene in 1938 and appear in his 1952 book Introduction to Metamathematics. A related theorem, which constructs fixed points of a computable function, is known as Rogers's theorem and is due to Hartley Rogers, Jr.

In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them. Any set that receives a classification is called arithmetical. The arithmetical hierarchy was invented independently by Kleene (1943) and Mostowski (1946).

In computability theory, a set S of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if:

In mathematical logic, the Löwenheim–Skolem theorem is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem.

In the foundations of mathematics, von Neumann–Bernays–Gödel set theory (NBG) is an axiomatic set theory that is a conservative extension of Zermelo–Fraenkel–choice set theory (ZFC). NBG introduces the notion of class, which is a collection of sets defined by a formula whose quantifiers range only over sets. NBG can define classes that are larger than sets, such as the class of all sets and the class of all ordinals. Morse–Kelley set theory (MK) allows classes to be defined by formulas whose quantifiers range over classes. NBG is finitely axiomatizable, while ZFC and MK are not.

In recursion theory, an elementary recursive function, also called an elementary function, or a Kalmár elementary function, is a restricted form of a primitive recursive function, allowing bounded applications of exponentiation.

Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form $and, where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic.$

In mathematical logic, Heyting arithmetic $is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.$

In computability theory, a function is called limit computable if it is the limit of a uniformly computable sequence of functions. The terms computable in the limit, limit recursive and recursively approximable are also used. One can think of limit computable functions as those admitting an eventually correct computable guessing procedure at their true value. A set is limit computable just when its characteristic function is limit computable.

In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.

In mathematical logic, a witness is a specific value $t$ to be substituted for variable $x$ of an existential statement of the form $\exists x φ (x)$ such that $φ (t)$ is true.

In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic, is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, $, together with induction for formulas with bounded quantifiers.$

References

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 from the 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". In van 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.

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.

Additional reading

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.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[1] reprinted in translation in van Heijenoort (1967)

[FOOTNOTETait1981-2] Tait 1981.

[FOOTNOTEKreisel1960-3] Kreisel 1960.

[4] Feferman (1998 , p. 4 (of personal website version)) Feferman differs from Kreisel's usage of 'finitism':^{[ clarification needed ]}
"The principle [of transfinite induction up to ε₀] may itself be justified on constructive grounds (though no longer clearly finitary grounds, even for decidable predicates.)" (emphasis added)

[1]

[2]

[3]

[4]