Primitive recursive arithmetic
Encyclopedia
Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem
as a formalization of his finitist conception of the 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, but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε0, 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 metamathematical formal system
for proof theory
, in particular for consistency proof
s such as Gentzen's consistency proof
of first-order arithmetic.
The logical axioms of PRA are the:
The logical rules of PRA are modus ponens
and variable substitution.
The non-logical axioms are:
and recursive defining equations for every primitive recursive function
desired, especially:
PRA replaces the axiom schema of induction
for first-order arithmetic with the rule of (quantifier-free) induction:
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
over all natural numbers. Defining primitive recursive function
s in this manner is not possible in PRA, because it lacks quantifiers.
gave the first such system. The rule of induction in Curry's system was unusual. A later refinement was given by Reuben Goodstein
. The rule of induction in Goodstein's system is:
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:
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:
Thus, the equations x=y and |x-y|=0 are equivalent. Therefore the equations
and 
express the logical conjunction
and disjunction, respectively, of the equations x=y and u=v. Negation
can be expressed as
.
Thoralf Skolem
Thoralf Albert Skolem was a Norwegian mathematician known mainly for his work on mathematical logic and set theory.-Life:...
as a formalization of his finitist conception of the foundations of arithmetic
Foundations of mathematics
Foundations of mathematics is a term sometimes used for certain fields of mathematics, such as mathematical logic, axiomatic set theory, proof theory, model theory, type theory and recursion theory...
, and it is widely agreed that all reasoning of PRA is finitist. Many also believe that all of finitism is captured by PRA, but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε0, 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
Natural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s and any primitive recursive function
Primitive recursive function
The primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the total µ-recursive functions...
, including the operations of addition
Addition
Addition is a mathematical operation that represents combining collections of objects together into a larger collection. It is signified by the plus sign . For example, in the picture on the right, there are 3 + 2 apples—meaning three apples and two other apples—which is the same as five apples....
, multiplication
Multiplication
Multiplication is the mathematical operation of scaling one number by another. It is one of the four basic operations in elementary arithmetic ....
, and exponentiation
Exponentiation
Exponentiation is a mathematical operation, written as an, involving two numbers, the base a and the exponent n...
. PRA cannot explicitly quantify over the domain of natural numbers. PRA is often taken as the basic metamathematical formal system
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
for proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, in particular for consistency proof
Consistency proof
In logic, a consistent theory is one that does not contain a contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if and only if it has a model, i.e. there exists an interpretation under which all...
s such as Gentzen's consistency proof
Gentzen's consistency proof
Gentzen's consistency proof is a result of proof theory in mathematical logic. It "reduces" the consistency of a simplified part of mathematics, not to something that could be proved , but to clarified logical principles.-Gentzen's theorem:In 1936 Gerhard Gentzen proved the consistency of...
of first-order arithmetic.
Language and axioms
The language of PRA consists of:- A countably infinite number of variables x, y, z,... each ranging over the natural numberNatural numberIn mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s. - The propositionalPropositional calculusIn mathematical logic, a propositional calculus or logic is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules and axioms allows certain formulas to be derived, called theorems; which may be interpreted as true...
connectives; - The equality symbol =, the constant symbol 0, and the successorPrimitive recursive functionThe primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the total µ-recursive functions...
symbol S (meaning add one); - A symbol for each primitive recursive functionPrimitive recursive functionThe primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the total µ-recursive functions...
.
The logical axioms of PRA are the:
- TautologiesTautology (logic)In logic, a tautology is a formula which is true in every possible interpretation. Philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921; it had been used earlier to refer to rhetorical tautologies, and continues to be used in that alternate sense...
of the propositional calculusPropositional calculusIn mathematical logic, a propositional calculus or logic is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules and axioms allows certain formulas to be derived, called theorems; which may be interpreted as true...
; - Usual axiomatization of equality as an equivalence relationEquivalence relationIn mathematics, an equivalence relation is a relation that, loosely speaking, partitions a set so that every element of the set is a member of one and only one cell of the partition. Two elements of the set are considered equivalent if and only if they are elements of the same cell...
.
The logical rules of PRA are modus ponens
Modus ponens
In classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
and variable substitution.
The non-logical axioms are:
-
; -
and recursive defining equations for every primitive recursive function
Primitive recursive function
The primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the total µ-recursive functions...
desired, especially:
-
-
-
-
- ... and so on.
PRA replaces the axiom schema of induction
Mathematical induction
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
for first-order arithmetic with the rule of (quantifier-free) induction:
- From
and 
, deduce 
, for any predicate 
In first-order arithmetic, the only primitive recursive function
Primitive recursive function
The primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the total µ-recursive functions...
s that need to be explicitly axiomatized are addition
Addition
Addition is a mathematical operation that represents combining collections of objects together into a larger collection. It is signified by the plus sign . For example, in the picture on the right, there are 3 + 2 apples—meaning three apples and two other apples—which is the same as five apples....
and multiplication
Multiplication
Multiplication is the mathematical operation of scaling one number by another. It is one of the four basic operations in elementary arithmetic ....
. All other primitive recursive predicates can be defined using these two primitive recursive functions and quantification
Quantification
Quantification has several distinct senses. In mathematics and empirical science, it is the act of counting and measuring that maps human sense observations and experiences into members of some set of numbers. Quantification in this sense is fundamental to the scientific method.In logic,...
over all natural numbers. Defining primitive recursive function
Primitive recursive function
The primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the total µ-recursive functions...
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 1941 Haskell CurryHaskell Curry
Haskell Brooks Curry was an American mathematician and logician. Curry is best known for his work in combinatory logic; while the initial concept of combinatory logic was based on a single paper by Moses Schönfinkel, much of the development was done by Curry. Curry is also known for Curry's...
gave the first such system. The rule of induction in Curry's system was unusual. A later refinement was given by Reuben Goodstein
Reuben Goodstein
Reuben Louis Goodstein was an English mathematician with a strong interest in the philosophy and teaching of mathematics....
. The rule of induction in Goodstein's system is:
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:
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:
Thus, the equations x=y and |x-y|=0 are equivalent. Therefore the equations
and express the logical conjunctionLogical conjunction
In logic and mathematics, a two-place logical operator and, also known as logical conjunction, results in true if both of its operands are true, otherwise the value of false....
and disjunction, respectively, of the equations x=y and u=v. Negation
Negation
In logic and mathematics, negation, also called logical complement, is an operation on propositions, truth values, or semantic values more generally. Intuitively, the negation of a proposition is true when that proposition is false, and vice versa. In classical logic negation is normally identified...
can be expressed as
.See also
- Elementary recursive arithmetic
- Heyting arithmeticHeyting arithmeticIn 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....
- Peano arithmetic
- Second-order arithmeticSecond-order arithmeticIn 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. It was introduced by David Hilbert and Paul Bernays in their...
- primitive recursive functionPrimitive recursive functionThe primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the total µ-recursive functions...
External links
- Feferman, SSolomon FefermanSolomon Feferman is an American philosopher and mathematician with major works in mathematical logic.He was born in New York City, New York, and received his Ph.D. in 1957 from the University of California, Berkeley under Alfred Tarski...
(1992) What rests on what? The proof-theoretic analysis of mathematics. Invited lecture, 15th int'l Wittgenstein symposium.