[FOM] "Recursive"

[Richard Zach]

> Skolem in his "Foundations of Elementary Arithmetic"
> of 1923 gives a formulation of what is now called
> primitive recursive arithmetic (in a free variable
> formalism), though he doesn't formally define the
> family of functions (it is implicit in
> his paper).

It should be noted perhaps that Skolem's paper is entirely informal,
i.e., he doesn't define a proof system or give the schema of primitive
recursion (as Alasdair mentioned).

> The first person to have singled out the family
> explicitly may have been Hilbert in 1925 in
> "On the infinite"; Ackermann's article of 1928
> "On Hilbert's Construction of the Real Numbers"
> singles out the same class.  The class was
> therefore one that was well known in the Hilbert
> school at the time, though Goedel's definition
> of 1931 was apparently the first completely
> formal specification of the family of primitive
> recursive functions.

In 1921/22, Hilbert held a course on foundations of mathematics in which
he sketches a formal system of primitive recursive arithmetic, including
a general statement of the schema of primitive recursion.  This is even
more clearly stated in a course from the following academic year,
co-taught with Bernays.  The relevant lecture was given by Bernays on
January 25, 1923, and the example definitions Bernays gives (minimum,
greatest common divisor) are different from Skolem's definitions, so
it's safe to assume this was carried out without knowledge of Skolem's
paper.  These lectures are currently being edited for publication and
will appear as vol. 3 in the series Hilbert's Foundational Lectures
(Springer; edited by Wilfried Sieg and Bill Ewald, I believe).

Ackermann's 1924 dissertation contains, I believe, the first published
formulation of primitive recursive arithmetic as a formal system.  It
also contains a consistency proof (using induction on ordinal notations
with order type < omega^omega^omega) for an (also formally specified)
system of second order primitive recursive arithmetic, i.e., where
functional parameters are allowed in the definitions. The Ackermann
function can be defined in this system. (It isn't actually defined in
the paper; Hilbert in "On the infinite" first mentions it.)

This system and the consistency proof are discussed in a paper which you
may find here:

http://www.ucalgary.ca/~rzach/papers/conprf.html

-Richard
-- 
Richard Zach ...... http://www.ucalgary.ca/~rzach/
Associate  Professor,   Department  of  Philosophy
University of Calgary, Calgary, AB T2N 1N4, Canada