H. P. Grice, "Communicatum and recursion"

The first work devoted exclusively to recursive definability was Skolem’s (1923) paper  The foundations of elementary arithmetic established by the recursive mode of thought, without the use of apparent variables ranging over infinite domains.  This work is significant with respect to the subsequent development of computability theory for at least three reasons. First, it contains a informal description of what we now call the primitive recursive functions. Second, it can be regarded as the first place where recursive definability is linked to effective computability (see also Skolem 1946). And third, it demonstrates that a wide range of functions and relations are primitive recursive in a manner which anticipates Gödel’s (1931) use of primitive recursion for the arithmetization of syntax.  One of Skolem’s stated goals was to present a logical foundation for number theory which avoids the use of unrestricted quantifiers. He was inspired in this regard by the observation that it is possible to develop much of elementary arithmetic without the use of the expressions “always” (i.e. for all) and “sometimes” (i.e. there exists) which figure in the formalization of number theory given by Russell and Whitehead in Principia Mathematica (1910–1913). This was to be accomplished by formulating arithmetical theorems as what he referred to as functional assertions. These took the form of identities between terms defined by primitive recursive operations which Skolem referred to as descriptive functions. For instance, the commutativity of addition is expressed in this form by an equation with free variables  x+y=y+x  In cases where such statements are provable in the system Skolem describes, the intended interpretation is that the claim holds universally for all natural numbers—e.g., ∀x∀y(x+y=y+x). But in Skolem’s system there is no means of negating such a statement to express a bare existential assertion without producing a witness.  Statements like (5) would later be referred to by Hilbert & Bernays (1934) (who provided the first textbook treatment of recursion) as verifiable in the sense that their individual instances can be verified computationally by replacing variables with concrete numerals. This is accomplished by what Skolem referred to as the “recursive mode of thought”. The sense of this phrase is clarified by the following properties of the system he describes:  the natural numbers are taken as basic objects together with the successor function x+1; it is assumed that descriptive functions proven to be equal may be substituted for one another in other expressions; all definitions of functions and relations on natural numbers are given by recursion; functional assertions such as (5) must be proven by induction. Taking these principles as a foundation, Skolem showed how to obtain recursive definitions of the predecessor and subtraction functions, the less than, divisibility, and primality relations, greatest common divisors, least common multiples, and bounded sums and products which are similar to those given in Section 2.1.2 below.  Overall Skolem considered instances of what we would now refer to as primitive recursion, course of values recursion, double recursion, and recursion on functions of type N→N. He did not, however, introduce general schemas so as to systematically distinguish these modes of definition. Nonetheless, properties i–iv of Skolem’s treatment provide a means of assimilating calculations like (2) to derivations in quantifier-free first-order logic. It is thus not difficult to discern in (Skolem 1923) the kernel of the system we now know as Primitive Recursive Arithmetic (as later formally introduced by Hilbert & Bernays 1934, ch. 7).