Primitive recursive arithmetic

Primitive recursive arithmetic

Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem [Thoralf Skolem (1923) "The foundations of elementary arithmetic" in Jean van Heijenoort, translator and ed. (1967) "From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931". Harvard Univ. Press: 302-33.] 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 [Tait, W.W. (1981) "J. of Philosophy 78": 524-46.] , but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε0 [Georg Kreisel (1958) "Ordinal Logics and the Characterization of Informal Notions of Proof," "Proc. Internat. Cong. Mathematicians": 289-99.] , which is the proof-theoretic strength of Peano arithmetic. PRA is sometimes called 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",... each ranging over the natural numbers.
*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:
* S(x) e 0;
* S(x)=S(y) o x=y,and recursive defining equations for every primitive recursive function desired, especially:
* x+0 = x
* x+S(y) = S(x+y)
* x cdot 0 = 0
* x cdot S(y) = xy + x
* ... and so on.PRA replaces the axiom schema of induction for first-order arithmetic with the rule of (quantifier-free) induction:
* mbox{From }phi(0)mbox{ and }phi(x) o phi(S(x))mbox{, deduce }phi(x)mbox{, for any predicate }phi.

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 sentences of PRA is just an equation between two primitive recursive functions of zero or more variables. In 1941 Haskell Curry gave the first such system [Haskell Curry, " [http://www.jstor.org/stable/2371522 A Formalization of Recursive Arithmetic] ". American Journal of Mathematics, vol 63 no 2 (1941) pp 263-282] , which had a non-elementary rule of induction. This was later refined by Reuben Goodstein [Reuben Goodstein, " [http://www.digizeitschriften.de/resolveppn/GDZPPN002343355 Logic-free formalisations of recursive arithmetic] ", Mathematica Scandinavica vol 2 (1954) pp 247-261] . The rule of induction in the latter 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 funcions which may have parameters other than the ones shown. The rules of substitution in this system are:

{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 primitive recursive functions of zero or more variables. Finally, as above, there are the defining equations for any primitive recursive functions needed.

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:

egin{align} P(0) = 0 quad & quad P(S(x)) = x \ x dot - 0 = x quad & quad x dot - S(y) = P(x dot - y) \
x - y| = & (x dot - y) + (y dot - x) \end{align}

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.

See also

* Heyting arithmetic
* Peano arithmetic
* Second-order arithmetic
* primitive recursive function

External links

* Feferman, S (1992) " [http://citeseer.ist.psu.edu/feferman92what.html What rests on what? The proof-theoretic analysis of mathematics] ". Invited lecture, 15th int'l Wittgenstein symposium.

References


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Primitive recursive function — The primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict subset of the recursive functions (recursive functions are also known as computable functions). The term was coined by… …   Wikipedia

  • Recursive set — In computability theory, a set of natural numbers is called recursive, computable or decidable if there is an algorithm which terminates after a finite amount of time and correctly decides whether or not a given number belongs to the set. A more… …   Wikipedia

  • Robinson arithmetic — In mathematics, Robinson arithmetic, or Q, is a finitely axiomatized fragment of Peano arithmetic (PA), first set out in Robinson (1950). Q is essentially PA without the axiom schema of induction. Even though Q is much weaker than PA, it is still …   Wikipedia

  • Arbitrary-precision arithmetic — In computer science, arbitrary precision arithmetic indicates that calculations are performed on numbers whose digits of precision are limited only by the available memory of the host system. This contrasts with the faster fixed precision… …   Wikipedia

  • Computability theory — For the concept of computability, see Computability. Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown …   Wikipedia

  • Recursion theory — Recursion theory, also called computability theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability… …   Wikipedia

  • List of algebraic structures — In universal algebra, a branch of pure mathematics, an algebraic structure is a variety or quasivariety. Abstract algebra is primarily the study of algebraic structures and their properties. Some axiomatic formal systems that are neither… …   Wikipedia

  • Outline of algebraic structures — In universal algebra, a branch of pure mathematics, an algebraic structure is a variety or quasivariety. Abstract algebra is primarily the study of algebraic structures and their properties. Some axiomatic formal systems that are neither… …   Wikipedia

  • Gödel's incompleteness theorems — In mathematical logic, Gödel s incompleteness theorems, proved by Kurt Gödel in 1931, are two theorems stating inherent limitations of all but the most trivial formal systems for arithmetic of mathematical interest. The theorems are of… …   Wikipedia

  • Dialectica interpretation — In proof theory, the Dialectica interpretation [1] is a proof interpretation of intuitionistic arithmetic (Heyting arithmetic) into a finite type extension of primitive recursive arithmetic, the so called System T. It was developed by Kurt Gödel… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”