that the consistency of a theory T implies the consistency of a theory S by producing a primitive recursive function that can transform any proof of an inconsistency from S into a proof of an inconsistency from T. One sufficient condition for a consistency proof to be finitistic is the ability to formalize it in PRA. For example, many consistency results in set theory that are obtained by forcing can be recast as syntactic proofs that can be formalized in PRA. History Recursive definitions had been used more or less formally in mathematics before, but the construction of primitive recursion is traced back to Richard Dedekind's theorem 126 of his Was sind und was sollen die Zahlen? (1888). This work was the first to give a proof that a certain recursive construction defines a unique function. Primitive recursive arithmetic was first proposed by Thoralf Skolem in 1923. The current terminology was coined by Rózsa Péter (1934) after Ackermann had proved in 1928 that the function which today is named after him was not primitive recursive, an event which prompted the need to rename what until then were simply called recursive functions. See also Grzegorczyk hierarchy Recursion (computer science) Primitive recursive functional Double recursion Primitive recursive set function Primitive recursive ordinal function Notes References Brainerd, W.S., Landweber, L.H. (1974), Theory of Computation, Wiley, Robert I. Soare, Recursively Enumerable Sets and Degrees, Springer-Verlag, 1987. Stephen Kleene (1952) Introduction to Metamathematics, North-Holland Publishing Company, New York, 11th reprint 1971: (2nd edition notes added on 6th reprint). In Chapter XI. General Recursive Functions §57 George Boolos, John Burgess, Richard Jeffrey (2002), Computability and Logic: Fourth Edition, Cambridge University Press, Cambridge, UK. Cf pp. 70–71. Robert I. Soare 1995 Computability and Recursion http://www.people.cs.uchicago.edu/~soare/History/compute.pdf Daniel Severin 2008, Unary primitive recursive functions, J. Symbolic Logic Volume 73, Issue 4, pp. 1122–1138 arXiv projecteuclid Computability theory Theory of computation Functions and mappings Recursion