For over two millennia mathematicians have used particular examples of algorithms for determining the values of functions. The notion of "λ-definability" was the first of what are now accepted as equivalent exact mathematical descriptions of the class of all number-theoretic functions for which algorithms exist. This article explains the notion, and traces the investigation in 1931-3 by which quite unexpectedly it was so recognized. The Herbrand-Gödel notion of "general recursiveness" 1934, and the Turing notion of "computability" 1936 were the second and third of the equivalent notions. Techniques developed in the study of λ-definability were applied in the analysis of general recursiveness and Turing computability.

Gödel has called to my attention that p. 773 is misleading in regard to the discovery of the finite axiomatization and its place in his proof of the consistency of GCH. For the version in [1940], as he says on p. 1, “The system Σ of axioms for set theory which we adopt [a finite one] … is essentially due to P. Bernays …”. However, it is not at all necessary to use a finite axiom system. Gödel considers the more suggestive proof to be the one in [1939], which uses infinitely many axioms. His main achievement regarding the consistency of GCH, he says, really is that he first introduced the concept of constructible sets into set theory defining it as in [1939], proved that the axioms of set theory (including the axiom of choice) hold for it, and conjectured that the continuum hypothesis also will hold. He told these things to von Neumann during his stay at Princeton in 1935. The discovery of the proof of this conjecture On the basis of his definition is not too difficult. Gödel gave the proof (also for GCH) not until three years later because he had fallen ill in the meantime. This proof was using a submodel of the constructible sets in the lowest case countable, similar to the one commonly given today.

I first heard the name of Kurt Gödel when, as a graduate student at Princeton in the fall of 1931, I attended a colloquium at which John von Neumann was the speaker, von Neumann could have spoken on work of his own; but instead he gave an exposition of Gödel's results of formally undecidable propositions [1931]. Today I shall begin with Gödel's paper [1930] onThe completeness of the axioms of the functional calculus of logic, or of what we now often call “the first-order predicate calculus”, using “predicate” as synonymous with “propositional function”. Alonzo Church wrote ([1944, p. 62] and [1956, pp. 288–289]), “the first explicit formulation of the functional calculus of first order as an independent logistic system is perhaps in the first edition of Hilbert and Ackermann'sGrundzüge der theoretischen Logik(1928).” Clearly, this formalism is not complete in the sense that each closed formula or its negation is provable. (Aclosed formula, orsentence, is a formula without free occurrences of variables.) But Hilbert and Ackermann observe, “Whether the system of axioms is complete at least in the sense that all the logical formulas which are correct for each domain of individuals can actually be derived from them is still an unsolved question.” [1928, p. 68]. This question Gödel answered in the affirmative in his Ph.D. thesis (Vienna, 1930), of which the paper under discussion is a rewritten version. I shall not describe Gödel's proof. Perhaps no theorem in modern logic has been proved more often than Gödel's completeness theorem for the first-order predicate calculus. It stands at the focus of a complex of fundamental theorems, which different scholars have approached from various directions (e.g. Kleene [1967, Chapter VI]).

This addendum supplies details of the proof in 3.6 of our paper Disjunction and existence under implication in elementary intuition-istic formalisms in this Journal, vol. 27 (1962), pp. 11–18, as promised in Footnote 8 of that paper (p. 16 lines 11 and 16, for “├” read “|”). A congruence-substitution (or free substitution with change of bound variables) on a formula E with result F consists in, simultaneously, substituting for each of the free variables of E in all its free occurrences a respective term and replacing each bound occurrence of a variable in E by a respective variable, so that (a) each image in F of a free occurrence of a variable in E is free (IM p. 410) and (b) each image in F of a bound occurrence of a variable in E is bound by the corresponding quantifier (i.e. if the j-th quantifier in E binds the original occurrence, then the j-th quantifier in F binds the image).

Let Pp, Pd, and N be the intuitionistic formal systems of prepositional calculus, predicate calculus, and elementary number theory, respectively.1 Consider the following six propositions.8 (1) ├A V B only if ├A or ├B. (2) ├∋xA(x) only if ├Ã(t) for some formula Ã(x) congruent to A(x) and some term t free for x in Ã(x).

The purpose of this article is to introduce the notion of “recursive realizability.” Let P be some property of natural numbers. Consider the existential statement, “There exists a number n having the property P.” To explain the meaning which this has for a constructivist or intuitionist, it has been described as a partial judgement, or incomplete communication of a more specific statement which says that a certain given number n, or the number n obtainable by a certain given method, has the property P. The meaning of the existential statement thus resides in a reference to certain information, which it implies could be stated in detail, though the trouble is not taken to do so. Perhaps the detail is suppressed in order to convey a general view of some fact. The information to which reference is made should be thought of as possibly comprising other items besides the value of n or method for obtaining it, namely such items as may be necessary to complete the communication that that n has the property P.

Consider a system of formal notations for ordinal numbers in the first and second number classes, with the following properties. Given a notation for an ordinal, it can be decided effectively whether the ordinal is zero, or the successor of an ordinal, or the limit of an increasing sequence of ordinals. In the second case, a notation for the preceding ordinal can be determined effectively. In the third case, notations for the ordinals of an increasing sequence of type ω with the given ordinal as limit can be determined effectively. Are there systems of this sort which extend farthest into the second number class? When the conditions for the systems have been made precise, the question will be answered in the affirmative. There is an ordinal ω1in the second number class such that there are systems of notations of the sort described which extend to all ordinals less than ω1, but none in which ω1itself is assigned a notation. 1. An effective or constructive operation on the objects of an enumerable class is one for which a fixed set of instructions can be chosen such that, for each of the infinitely many objects (orn-tuples of objects), the operation can be completed by a finite process in accordance with the instructions. This notion is made exact by specifying the nature of the process and set of instructions. It appears possible to do so without loss of generality.