Only Two Letters: The Correspondence between Herbrand and Gödel

Two young logicians, whose work had a dramatic impact on the direction of logic, exchanged two letters in early 1931. Jacques Herbrand initiated the correspondence on 7 April and Kurt Gödel responded on 25 July, just two days before Herbrand died in a mountaineering accident at La Bérarde (Isère). Herbrand's letter played a significant role in the development of computability theory. Gödel asserted in his 1934 Princeton Lectures and on later occasions that it suggested to him a crucial part of the definition of a general recursive function. Understanding this role in detail is of great interest as the notion is absolutely central. The full text of the letter had not been available until recently, and its content (as reported by Gödel) was not in accord with Herbrand's contemporaneous published work. Together, the letters reflect broader intellectual currents of the time: they are intimately linked to the discussion of the incompleteness theorems and their potential impact on Hilbert's Program.

A note on the representation of general recursive functions and the μ quantifier

It has been shown that every general recursive function is definable by application of the five schemata for primitive recursive functions together with the schemasubject to the condition that, for each n–tuple of natural numbers x1,…, xn there exists a natural number xn+1 such that

Arithmetical representation of recursively enumerable sets

A set S of natural numbers is called recursively enumerable if there is a general recursive function F(x, y) such thatIn other words, S is the projection of a two-dimensional general recursive set. Actually, it is no restriction on S to assume that F(x, y) is primitive recursive. If S is not empty, it is the range of the primitive recursive functionwhere a is a fixed element of S. Using pairing functions, we see that any non-empty recursively enumerable set is also the range of a primitive recursive function of one variable.We use throughout the logical symbols ⋀ (and), ⋁ (or), → (if…then…), ↔ (if and only if), ∧ (for every), and ∨(there exists); negation does not occur explicitly. The variables range over the natural numbers, except as otherwise noted.Martin Davis has shown that every recursively enumerable set S of natural numbers can be represented in the formwhere P(y, b, w, x1 …, xλ) is a polynomial with integer coefficients. (Notice that this would not be correct if we replaced ≤ by <, since the right side of the equivalence would always be satisfied by b = 0.) Conversely, every set S represented by a formula of the above form is recursively enumerable. A basic unsolved problem is whether S can be defined using only existential quantifiers.

The recursive irrationality of π

A primitive-recursive sequence of rational numbers sn is said to be primitive-recursively irrational, if there are primitive recursive functions n(k), i(p, q) > 0 and N(p, q) such that:1. (k)(n ≥ n(k) → ∣sn – sn(k)∣ < 2−k).2. (p)(q)(q > 0 & n ≥ N(p, q) → ∣sn ± p/q∣ > 1/i(p, q)).The object of the present note is to establish the primitive-recursive irrationality of a sequence which converges to π. In a previous paper we proved the primitive-recursive irrationality of the exponential series Σxn/n!, for all rational values of x, and showed that a primitive-(general-) recursively irrational sequence sn is strongly primitive-(general-)recursive convergent in any scale, where a recursive sequence sn is said to be strongly primitive-(general-)recursive convergent in the scale r (r ≥ 2), if there is a non-decreasing primitive-(general-) recursive function r(k) such that,where [x] is the greatest integer contained in x, i.e. [x] = i if i ≤ x < i + 1, [x] = —i if i ≤ —x < i+1, where i is a non-negative integer.A rational recursive sequence sn is said to be recursive convergent, if there is a recursive function n(k) such that.If a sequence sn is strongly recursive convergent in a scale r, then it is recursive convergent and its limit is the recursive real number where, for any k ≥ 0,.

A note on nominalism and recursive functions

The purpose of this note is (i) to point out an important similarity between the nominalistic system discussed by Quine in his recent paper On universals and the system of logic (the system н) developed by the author in A homogeneous system for formal logic, (ii) to offer certain corrections to the latter, and (iii) to show that that system (н) is adequate for the general theory of ancestrale and for the definition of any general recursive function of natural numbers.Nominalism as a thesis in the philosophy of science, according to Quine, is the view that it is possible to construct a language adequate for the purposes of science, which in no wise admits classes, properties, relations, or other abstract objects as values for variables.

Computability and λ-definability

Several definitions have been given to express an exact meaning corresponding to the intuitive idea of ‘effective calculability’ as applied for instance to functions of positive integers. The purpose of the present paper is to show that the computable functions introduced by the author are identical with the λ-definable functions of Church and the general recursive functions due to Herbrand and Gödel and developed by Kleene. It is shown that every λ-definable function is computable and that every computable function is general recursive. There is a modified form of λ-definability, known as λ-K-definability, and it turns out to be natural to put the proof that every λ-definable function is computable in the form of a proof that every λ-K-definable function is computable; that every λ-definable function is λ-K-definable is trivial. If these results are taken in conjunction with an already available proof that every general recursive function is λ-definable we shall have the required equivalence of computability with λ-definability and incidentally a new proof of the equivalence of λ-definability and λ-K-definability.A definition of what is meant by a computable function cannot be given satisfactorily in a short space. I therefore refer the reader to Computable pp. 230–235 and p. 254. The proof that computability implies recursiveness requires no more knowledge of computable functions than the ideas underlying the definition: the technical details are recalled in §5.

Extensions of some theorems of Gödel and Church

We shall say that a logic is “simply consistent” if there is no formula A such that both A and ∼ A are provable. “ω-consistent” will be used in the sense of Gödel. “General recursive” and “primitive recursive” will be used in the sense of Kleene, so that what Gödel calls “rekursiv” will be called “primitive recursive.” By an “Entscheidungsverfahren” will be meant a general recursive function ϕ(n) such that, if n is the Gödel number of a provable formula, ϕ(n) = 0 and, if n is not the Gödel number of a provable formula, ϕ(n) = 1. In specifying that ϕ must be general recursive we are following Church in identifying “general recursiveness” and “effective calculability.”First, a modification is made in Gödel's proofs of his theorems, Satz VI (Gödel, p. 187—this is the theorem which states that ω-consistency implies the existence of undecidable propositions) and Satz XI (Gödel, p. 196—this is the theorem which states that simple consistency implies that the formula which states simple consistency is not provable). The modifications of the proofs make these theorems hold for a much more general class of logics. Then, by sacrificing some generality, it is proved that simple consistency implies the existence of undecidable propositions (a strengthening of Gödel's Satz VI and Kleene's Theorem XIII) and that simple consistency implies the non-existence of an Entscheidungsverfahren (a strengthening of the result in the last paragraph of Church).