Below is the uncorrected machine-read text of this chapter, intended to provide our own search engines and external engines with highly rich, chapter-representative searchable text of each book. Because it is UNCORRECTED material, please consider the following text as a useful but insufficient proxy for the authoritative book pages.

· ~ KURT GODEL April 28, 1906-January 14, 1978 BY STEPHEN C. KLEENE1 TW O P A P E R S ~ ~ 930a, ~ 93 ~ a), both written before the au- thor reached the age of twenty-five, established Kurt Go- de! as second to none among logicians of the modern era, beginning with Frege (18791.2 A third fundamental contri- bution followed a little later ~ ~ 93Xa, ~ 93Sb, ~ 939a, ~ 939b). ORIGINS AND EDUCATION, 1906-1930 Gocle} was born at Brunn in the Austro-Hungarian prov- ince of Moravia. After World War I, Brunn became Brno in Czechoslovakia. Goclel's father Rudolf was managing director and partial owner of one of the leaching textile firms in Brunn; his family had come from Vienna. His mother Mar- ianne had a broad literary education. Her father, Gustav Handschuh, had come from the Rhineland. Godel's family cultivated its German national heritage. After completing secondary school at Brno, in 1924 Go- de] went to Vienna to study physics at the university. The elegant lectures of P. Furtwangler (a pupil of Hilbert and cousin of the famous conductor) fed his interest in mathe ~ For some details of Godel's life, I have drawn upon Kreisel (1980) and Wang (1978, 1981); the authors kindly supplied me with copies. 2 A date shown in parentheses refers to a work listed in the References (or for Godel, in the Bibliography), under the name of the adjacent author. 135

136 BIOGRAPHICAL MEMOIRS matics, which became his major area of study in 1926. His principal teacher was the analyst Hans Hahn, who was ac- tively interested in the foundations of mathematics. Hahn was a member of the Vienna Circle (Wiener Kreis), the hand of positivist philosophers led by M. Schlick, who was assassi- nated during a lecture in ~ 936. Gocle} attended many of their meetings, without subscribing to all of their doctrines (see Wang 1981, 6531. His doctoral dissertation was completect in the autumn of 1929, and he receiver! the Ph.D. on February 6, 1930. A somewhat reviser! version was presented at Karl Menger's colloquium on May 14, 1930, and was published (1930a) using "several valuable suggestions" of Professor Hahn "regarding the formulation for the publication" (Wang 1981, 654; 1930b is an abstract). GODEL S COMPLETENESS THEOREM ~1930a) Since Frege, the tractitional subject-preclicate analysis of the structure of sentences has been replaced by the more flexible use of propositional functions, or, more briefly, predi- cates.3 Using a given collection or domain D of objects (we call them individuals if they are the primary objects not being analyzecI) as the range of the independent variables, a one- place predicate P or P(a) over D (also callecI a property of mem- bers of D) is a function that, for each member of D as value of the variable a, takes as its value a proposition P(a). A two- place predicate Q or Q(a,b) (also called a binary relation be- tween members of D), for each pair of values of a ant! b from D, takes as value a proposition Q(a,b); ant! so on. In the most commonly cultivated version of logic (the classical logic), the 3 I am endeavoring to give enough background material to enable a scientist who is not a professional mathematician and not already acquainted with mathematical logic to understand Godel's best-known contributions. The memoir (1980) by Krei- sel, about three times the length of the present one, includes many interesting details addressed to mathematicians, if not just to mathematical logicians. The memoir (1978) by Quine gives an excellent overview in just under four pages.

.. KURT GODEL 137 propositions taken as values of the predicates are each either true or false. The restricted or f rst-order predicate calculus ("elementary logic") deals with expressions, callecIformulas, constructed, in accordance with states! syntactical rules, from: variables a, b, c, ..., x, y, z for individuals; symbols P. Q. R. S. ... for precli- cates; the propositional connectives , ("not"), & ("ancl"), V ("or") and ~ ("implies"~; and the quantifiers Nix ("for all x") and 3x ("Ethere] exists fan] x Esuch thatch. For example, taking P. Q. R to be symbols for predicates of one, two, and three variables, respectively, the expressions P(b), Q(a,c), R(b,a,a), NlxP(x), VxSyQfx,y), Vx(( ,P(x)) ~ Q(a,x)), and Vx(~3yQfy,x)) ~ R(x,a,x)) are formulas. In the classical logic, after making any choice of a non- empty domain D as the range of the variables, each formula can be evaluated as either true or false for each assignment in D of a predicate over D as the value or interpretation of each of its predicate symbols, and of a member of D as the value of each of its "free" variables. Its free variables are the ones with "free" occurrences, where they are not operated upon by quantifiers. In the seven examples of formulas given above, the eight occurrences of a, b, and c are free; the fifteen occurrences of x and y are not free, that is, they are bound. The evaluation process is straightforwarcl, taking V to be the inclusive "or" (A V B is true when one or both of A and B are true, and false otherwise), and handling A ~ B like ~ ~A) V B. For example, taking D to be the non-negative in- tegers or natural numbers i,0, i, 2, ...l, and assigning to P(a), Q(a,b) and R(a,b,c) the predicates "a is even", "a is less than b" and "ab = c", anti to a, b, and c the numbers 0, I, and 1, as values, our seven examples of formulas are respectively false, true, true, false, true, true, and true. Logic is concerned with exploring what formulas express logical truths, that is, are "true in general". LeiLnitz spoke of

38 BIOGRAPHICAL MEMOIRS truth in all possible worlds. We call a formula valid in D (a given non-empty domain) if it is true for every assignment in D; and simply valid if it is valid in every non-empty do main D. To make reasoning with the predicate calculus practical, paralleling the way we actually think, we cannot stop to think through the evaluation process in all non-empty domains for all assignments each time we want to assure ourselves that a formula is logically true (valid). Instead we use the "axio- matic-deductive method", whereby certain formulas become "provable". First, certain formulas are recognized as being logical ax- ioms. For example, all formulas of either of the following two forms-the forms being called axiom schemata are axioms: A > (B~A). b~xA(x) ~ A(a). Here A, B. and A(x) can be any formulas, and x and a any variables; A(a) is the result of substituting the variable a for the free occurrences of the variable x in the formula A(x). Furthermore, it is required that the resulting occurrences of a in A(a) be free; thus b~x3bQfb,x) > 3bQfb,a) is an axiom by the schema NlxA(x) ~ A(a), but NlxBaQ(a,x) ~ 3aQ(a,a) is not. The axiom schemata (and particular axioms, if we have some not given by schemata) are chosen so that each axiom is valid. Second, circumstances are recognized, called rules of infer- ence, in which, from the one or two formulas shown above the line called premises, the formula shown below the line called the conclusion can be inferred; for example: A, A ~ B B. (I ~ A(x) C ~ 3xA(x). Here A, B. and A(x) can be any formulas, x any variable, and C any formula not containing a free occurrence of x. The

as KURT GODEL 139 rules of inference are chosen so that, whenever for a given non-empty domain D and assignment in D the premises are true, then for the same D ant! assignment the conclusion is true. Hence, if the premises are valict, the conclusion is valid. A proof is a finite list of formulas, each one in turn being either an axiom or the conclusion of an inference from one or two formulas earlier in the list as the promisers). A proof is a proof of its last formula, which is said to be provable. In one of the stanciard treatments of the classical first- order predicate calculus (Kleene ~ 952, X2), twelve axiom schemata and three rules of inference are usecI.4 By what we have just said about how the axiom schemata (or particular axioms) are chosen (so each axiom is valid), and likewise the rules of inference (so truth is carried for ward by each inference), every provable formula is valid. Thus the axiomatic-deductive treatment of the predicate calculus is correct. But is it complete? That is: Is every vali~formula provable? The axiomatic-clecluctive treatment of the first-orcler predicate calculus, separated out from more complicated log- ical systems, was perhaps first formulated explicitly in Hilbert anct Ackermann's book (19284. The completeness problem was first stated there (p. 681: "Whether the system of axioms [and rules of inference] is complete, so that actually all the logical formulas which are correct for each domain of indi- viduals can be derives! from them, is still an unsolved ques- tion." It is this question that Gode! answered in (1930a). He es- tablished: For each formula A of thefirst-order predicate calculus, either A is provable in it, or A is not valid in the domain 10, I, 2, ...) of the natural numbers (and therefore is not valicl). So, if A is valid, then Goclel's second alternative is excluded, 4 I am giving the version of the predicate calculus with predicate symbols instead of predicate variables, after von Neumann (1927). This I consider easier to explain.

140 BIOGRAPHICAL MEMOIRS and A is provable. This answers Hilbert and Ackermann's question affirmatively. Let us say that a formula A is (or several formulas are simultaneously) satisf able in a given domain D if A is satisfied (all the formulas are satisfied), that is, made true, by some assignment in D. Then A-is-satisfiable-in-D is equivalent to , A-is-not-valicl-in-D. Now if A is satisf able in some domain D, then ,A is not valid in that domain D, so MA is not valict, so ,A is not provable (by the correctness of the predicate calculus), so by Godel's result appliers to A, MA is not valid in {0, i, 2, ...}, so A is satisfiable in {O. I, 2, ...~. This is a theorem of Lowenheim (1915~. Restating the completeness theorem for ,A: Either MA Is not valid (that is, A is satisfiable) in 10, I, 2, ...), or ,A is provable (equivalently, a contradiction can be cleducecT from A). Gocle} also treated the case for an infinite collection of formulas {Ao' A1, A2, ...} in place of one formula. The result is just what comes from substituting {Ao' A1, A2, ...} for A in the immediately preceding statement, and noting that, if a contradiction can be deducecI from the formulas Ao, A1, A2, ..., only a finite number of them can participate in a given deduction of the contradiction. Thus: Either the formulas Ao, A1. Air ... are simultaneousiv satisfiable in 10, I, 2....T, or, for some . 1' A' ~ J ' ' ' ' ' ' ' ~J 6~]tD C1lhCDt 1~ A I ~t them .{A ~ ~ A ~ it ~rn7JohiP J~1Vvvv ~"V~ovv En ail, ···' ~ Hind VJ VlVvllV, I `' JO ~ ~ ~ ~j J TV r. ~vw~vv {art hunt Girl cry A 1 -rid \~A4~ A4~ ,, ~ ^^il, ..., Ai are not simultaneously satis- fiable in any clomain). Now, if the formulas of each finite subset of {Ao' A1, A2, ...) are simultaneously satisfiable in a respective domain, then the second alternative just above is exclucled, so all the formulas are simul- taneously satisf able (this result is called "compactness"), indeed in the domain {0, i, 2, ...} (the Lowenheim-Skolem theorem). Skolem in (1920), in addition to closing up a gap in Lowen

.. KURT GODEL 141 helm's (1915) reasoning, added the case of infinitely many formulas. These satisfiability results, which are coupled with the completeness theorem in Godel's treatment, have surprising consequences in certain cases when we aim to use a collection of formulas as axioms to characterize a mathematical system of objects. In doing so, the formulas are not to be logical axioms, but rather mathematical axioms intended to be true, for a given domain D and assignment of predicates over D to the predicate symbols, exactly when D and the predicates have the structure we want the system to have. To make the evaluation process apply as intended, ~ shall suppose the ax- ioms to be closed, that is, to have no free variables. In using the symbolism of the predicate calculus to for- muiate mathematical axioms, we usually want to employ a predicate symbol E(a,b) intended to express a = b, and usually written a=b. Then, for our evaluation process we are only interested in assignments that give E(a,b) the value a= b, that is, that make E(a,b) true exactly when a and b have the same member of D as value. Adding some appropriate axioms to the predicate calculus for this case (Kleene 1952, top 399), we get the f rst-order predicate calculus with equality. Godel of- fered supplementary reasoning that adapted his treatment for the predicate calculus to the predicate calculus with equality, with "the domain {0, I, 2, ...~" being replaced in his conclusions by "~0, I, 2, ...) or a non-empty finite domain". Cantor in (~874) established that the set of all the subsets of the natural numbers {0, I, 2, ...) (or the set of the sets of natural numbers) is more numerous, or has a greater cardinal number, than the set of the natural numbers. To explain this, ~ review some notions of Cantor's theory of sets. He wrote (~895, 4814: "By a 'set' we understand any collection M of definite well-distinguished objects m of our perception or our thought (which are called the 'elements' for 'members'] of M)

142 BIOGRAPHICAL MEMOIRS into a whole." A set N is a subset of a set M if each member of N is a member of M. For example, the set {0, 1, 2} with the three members shown has the following ~ (= 23) subsets: {0, I, 2), {l, 2), {0, 2), {0, i}, {0}, Ail, {2), ~ }. Cantor showocl that there is no way of pairing all the sets of natural numbers (that is, all the subsets of the natural numbers) with the natural numbers, so that one subset is paired with 0, another with I, still another with 2, and so on, with every natural number used exactly once. Sets have the same cardinal number if they can be thus paired with each other, or put into a "one-to-one correspondence". Denoting the cardinal number of the nat- ural numbers by R0, anc! adopting No as a notation for the cardinal of the sets of natural numbers, thus No ~ 80. But the natural numbers can be paired with a subset of the sets of natural numbers (incleed with the unit sets I,O'J, ISIS, {2i, ... having one member each), so we write No ~ R0. Sets that are either finite or have the cardinal He are called countable; other sets, uncountable. The real numbers (corre- sponding to the points on a line) have the same cardinal No as the sets of natural numbers. ~ have been tacitly assuming for the first-orcl~er predicate calculus (without or with equality) that only a countable col- lection of variables and of predicate symbols is allowed. This entails that only a countable collection of formulas exists. Now suppose that we want to write a list of formulas A,,, ..., An or Ao' Al, A2, ... in the first-order predicate calculus with equality to serve as axioms characterizing the sets in some version of Cantor's theory of sets. Presuming that the axioms are satisfied simultaneously in some domain D (the "sets" in that version of Cantor's set theory) by some assign ment (the on-e understood in his theory), it follows by the Lowenheim-Skolem theorem that they are also satisfiable in the countable domain 10, i, 2, ...~! (It is evident that they are not satisfiable in a finite domain.) That is, one can so interpret

·. KURT GODEL 143 the axioms that the range of the variables in them constitutes a countable collection, contradicting the theorem of Cantor by which the subsets of {0, I, 2, ...} (which are among the sets for his theory) constitute an uncountable collection. This is Skolem's paradox (19231. It is not a direct contradiction; it only shows that we have failecI by our axioms to characterize the system of all the sets for Cantor's theory, as we wished to do. Suppose instead that we want a list of formulas Ao, Al, A2, in the first-order predicate calculus with equality to serve as axioms characterizing the system of the natural numbers 0, I, 2, .... Skolem in (1933, 1934) showed that we cannot succeed in this wish. He constructed so-called "non-standarct moclels of arithmetic", mathematical systems satisfying all the axioms An, Al, As, ... (or indeecI all the formulas that are true in the arithmetic of the natural numbers) but with a clifferent structure (as the mathematicians say, not isomorphic to the nat- ural numbers). In fact, as seems to have been noticec! first by Henkin in (1947), the existence of non-stanclarct models of arithmetic is an immediate consequence of the compactness part of Goclel's completeness theorem for the predicate cal- culus with equality. Before giving Henkin's argument, I observe that we may enlarge the class of formulas for the first-order predicate calculus with equality by allowing individual symbols i, j, k, .... which for any assignment in a domain D are given members of D as their values, and function symbols f, g, h, ..., where, for example, if f is a symbol for a two-place function, its inter- pretation in any assignment is as a function of two variables ranging over D and taking values in D. Examples that come to mincI for systems of axioms for the natural numbers are O as an incTiviclual symbol (with the number O as its stanciard interpretation), ' as a one-place function symbol (to be inter- pretect by + I), and + and x as two-place function symbols

44 BIOGRAPHICAL MEMOIRS (for addition and multiplication). Such additions to the sym- bolism are not essential. We couIcI equivalently use predicate symbols Z(a), S(a,b), A(a,b,c), and M(a,b,c), where Z(a) is taken as true exactly when the value a of a is O; S(a,b) when a+ ~ = b; A(a,b,c) when a+ b = c; anti M(a,b,c) when ab = c. Here "equivalently" means that whatever can be expressed using the indiviclual and function symbols can be para- phrased using the predicate symbols (but at a considerable loss of convenience). This is shown in Hilbert and Bernays (1934, 460 95.) and Kleene (1952, §741. Now take the proposed list of axioms Ao' Al, A2, ..., which are true under the interpretation by the system of the natural numbers. I shall assume they include (or if necessary add to them) the axioms Vxfx'=O) and Vx~y~x'=y' ~ x=y). Now consider instead the list Ao' ,i = 0, Al, pi = 0', A2, ,i = 0", ... where i is a new individual symbol. Each finite subset of these formulas is true under the intencled interpretation of the oIct symbols and interpreting i by a natural number n for which ~i= 0`n' (with n accents on the 0) is not in the subset. So by compactness, Ao' ~i= 0, Al, ~i= 0', A2, ~i= 0", ... are simultaneously satisfiable. It is easy to see that the satisfying system is isomorphic to one in which 0, i, 2, ... are the values of 0, 0', 0", ... and the value of i is not a natural number a non-stanciard mocle! of arithmetic. These illustrations will suggest the power of Goclel's com- pleteness theorem (1930a) with its corollaries as a too} in studying the possibilities for axiomatically founding various mathematical theories. Actually, not only was the Lowenheim-Skolem theorem around earlier than 1930, but it has been noticed in retro- spect that the completeness of the first-order predicate cal- culus can be derived as an easy consequence of Skolem (19231. Nevertheless, the possibility was overIookecl by Sko- lem himself; indeed the completeness problem was first for

.. KURT GODEL 145 mulatect in Hilbert-Ackermann (192X). Skolem workocT with logic intuitively rather than using an explicitly describecl set of axioms and rules of inference. Goclel's treatment of the problem in (1930a) was done without knowlecige of Skolem (1922), which Hilbert ant! Ackermann do not mention, and was incisive, obtained the compactness, and incluclecI the sup- plementary argument to make it apply to the predicate cal- culus with equality. VIENNA, WITH VISITS TO PRINCETON (lAS) 1 930-1 939 Godel's father cried in 1929, and Goclel's mother moved to Vienna. She took a large flat and sharer! it with her two sons, until she returned to her beautiful villa in Brno in 1937. Rudolf, the elcler son, was already a successful ractiologist in Vienna. The theater in Vienna appealed to her literary in- terests, and the sons went with her. Gocle] began in 1930 to work on the consistency problem of Hilbert's formalist school, which I will describe in the next section. His approach to this (as clescribecl in Wang (1981, §21) lecT him to some results on unclecidable propositions (preliminary to 1931a), which he announced at a meeting in September 1930 at Konigsberg (1930c). von Neumann was much interested anc! hac! some penetrating discussions with Godel, both at the meeting and by correspondence. In No- vember 1930, Goclel's famous paper (1931a) was completed ant! sent to the Monatshefte Received November 17, 19301. It was accepted] by Hahn as Godel's Habilitationsschrift on Tanu- ary 12, 1932. (19306) and (1930e) are abstracts of it and (193 I ct) is relevant to it. From 1931 through 1933 Gocle! attencled Hahn's seminar on set theory (Hahn died in 1934), and took part in Karl Menger's colloquium, which yielclecl proceedings that re- portect a number of Godel's results. In 1933 he was appointed

46 BIOGRAPHICAL MEMOIRS a Privatdozent (an unpaid lecturer) at Vienna. In the academic year 1933-34, he went to Princeton as a visitor at the Insti- tute for Advanced Study, and lecturecI on his (1931a) results; Rosser and I took the notes (1934~. He again visited the IAS in the fall of 1935. While he was there (according to Kleene (1978) and Wang (1981, Footnote 74), he toict van Neumann of his plan for proving the relative consistency of the axiom of choice anct the continuum hy- pothesis by use of his concept of "constructible sets". He com- plete(1 his plan three years later ~ ~ 938a, ~ 938b, ~ 939a, 1939b), as will be discussed in the second section below. On September 20, 1938, he married Aclele Porkert. (She survived him by three years, passing away on February 4, 1981.) He returned to the lAS in Princeton in the fall of 1938. In the spring of 1939 he lectured at Notre Dame, and he returned to Vienna in the fall of 1939. Godel's mother, almost alone among her friends and neighbors, tract been skeptical of the successes of Germany uncler Hitler. In March 1938, when Austria became a part of Germany and the title of Privatdozent was abolishecI, Gode} was not macle a Dozent never Ordnung, (paicI) lecturer of the new order, as were most of the university lecturers who had held the title of Privatdozent. He was thought to be Jewish, and once for this reason he was attacked in the street by some rowdies. Concerning his application of 25 September 1939 for a Dozentur never Ordnung, the Dozentenbundsfahrer wrote on 30 September 1939 (without supporting or rejecting the application) that Gode! was not known ever to have uttered a single word in favor of or against the National Socialist movement, although he himself moved in ~ewish-liberal circles, though with mitigating circumstances. (The applica- tion was actually accepted! on 28 June 1940, when Gocle} was no longer available.) Gode} was bitterly frustrated. He was apprehensive that he might be conscripted into the German

.. KURT GODEL 147 army, despite his frail health, which he believed renclered him unfit for military service. So at the end of 1939, he re- turnecI to Princeton, crossing the U.S.S.R. on the Trans- Siberian Railway. As a sequel, his mother stayed at her villa in Brno. She was openly critical of the National Socialist regime (thereby losing most of her former friends), so she did not expect reprisals by the Czechs. She returned to Vienna in 1944. But after the war, under the treaty between the Austrian govern- ment and Czechoslovakia, she received for her villa only a tenth of its assessed value. GODEL S INCOMPLETENESS THEOREMS (I93la), ETC. Cantor's development of set theory, begun in (~874), hacI led - beginning in IS95 to the discovery of paradoxes in it by himself, Cesari Burali-Forti, Bertrand Russell, and Jules Richard. For a quick illustration, ~ state the Russell: paradox (for the others, and references, see Kleene (1952, § ~ 1~. Rus- sell considered the set T of all those sets that are not members of themselves, which seemed to come uncler Cantor's defini- tion of 'set', quoted above. Is T a member of T? In symbols, does T ~ T? Suppose T ~ T; then by the definition of T. not T ~ T (in symbols T ~ T), contradicting the supposition. So by recluctio ad absurclum, T ~ T. Similarly, supposing T ~ T. Te T. Thus both Ti T and Te T! The appearance of the paradoxes gave special impetus to thinking about the foundations of mathematics, beyond what was already called for by the very extensive reformulations of various branches of mathematics in the nineteenth cen- tury. By the mict-1920s, three principal schools of thought had evolvecl. The logicistic school was represented by Bertrand Russell and Alfred North WhiteheacI. It proposed to make mathe- matics a branch of logic, in accordance with Leibnitz's 1666

148 BIOGRAPHICAL MEMOIRS conception of logic as a science containing the ideas ant! prin- ciples unclerlying all other sciences. They proposed to cle- duce the bocly of mathematics from logic, continuing from work of Frege, Declekind, and Peano (see Kleene 1952, 43- 461. To avoid the newly discovered paradoxes, Russell for- mulate(l his theory of types (1908), in which the indivicluals (or primary objects not being subjected to analysis) are as- signed to the lowest type 0, the properties of in(livicluals (or one-place predicates over type 0) to type I, the properties of type- ~ objects to type 2, anti so on. A rather definite structure was assumed for the totality of the possible definitions of objects of a given type. The clecluction on this basis of a very large portion of the existing mathematics was carried out in the monumental Principia Mathematica (PM) of Whitehead and Russell in three volumes ~ ~ 9 ~ 0, ~ 9 ~ 2, ~ 9 ~ 31. Neither of the other two schools, the intuitionistic and the formalistic, agreed to start back in logic to deduce the simplest parts of mathematics, such as the elementary theory of the natural numbers 0, I, 2, .... IncleecT, it can be argued that mathematical conceptions on this level are aIreacly presup- posect in the formulation of logic with the theory of types. The intuitionistic school of thought dates from a paper of Brouwer (1908) criticizing the prevailing or "classical" logic and mathematics. Brouwer argued that classical logic and mathematics go beyond intuition in treating infinite collec- tions as actually existing. As an example, each of the natural numbers 0, I, 2, ... is a finite object; but there is no last one. Mathematicians can often establish that a property is pos- sessed by every natural number n by reasoning that involves working with only the natural numbers out to a certain point depending on n (maybe just with the numbers ' n). Thus the infinity is only a potential infinity (an horizon within which we work). On the other hand, much of the existing classical mathematics deals with infinite collections as completecl or

.. KURT GODEL 149 actual infinities. Some reasoning with the natural numbers uses an actual infinite; for example, the application of the law of the excluded miclcIle to say that either some natural num- ber has a certain property P. or that is not the case (so every natural number has the property not-P). The use of infinite collections as actual infinities is pervasive in the usual theory of the real numbers, represented! say using infinite decimals. Brouwer, in papers beginning in 1918 (exposition in Heyting 1971), proposed to see how far mathematics couIct be recle- veloped using only methods that he consiclered intuition as justifying: that is, methods using only potential infinities, not actual ones. Brouwer was able to go rather far in this clirec- tion, at the cost of altering the subject substantially from the classical form as typified by the classical analysis that physi- cists are accustomed to applying. The formalistic school was initiated by Hilbert in (1904), and he clevelopecI it with a number of collaborators after 1920. Hilbert agreed with the intuitionists that much of cIas- sical mathematics goes beyond intuitive evidence. He drew a ctistinction between real statements in mathematics, which have an intuitive meaning, and ideal statements, which do not but in classical mathematics are adjoinect to the real ones to make mathematical theories simpler ancT more comprehen- sive. His real statements are those that correspond to the use of infinity only potentially, while an actual infinite is involved in the ideal statements. But rather than simply abandoning the ideal parts of mathematics, Hilbert had another proposal. We saw above how the first-order predicate calculus, after logical propositions are expressed as formulas in a precisely regulated symbolic language, was organized by the axio- matic-cleductive method. Whiteheact and Russell, and Hil- bert, proposed to do the same for mathematics generally, that is for very substantial portions of mathematics short of the paradoxes. As we saw, Whitehead and Russell proposer] to

150 BIOGRAPHICAL MEMOIRS make all of it logic, but not just first-order logic, within which mathematics is to be defined. Instead, Hilbert proposed to start with mathematical axioms as well as logical axioms. This can be done in the symbolism of the first-orcler predicate calculus, or using a second-order predicate calculus (with quantification of properties of inclivicluals), or still higher- orcler predicate calculi. In proofs in a system obtained by adding mathematical axioms to the logical apparatus of the first-order predicate calculus (or, as we may call them, "de cluctions" by logic from the mathematical axioms), we are exploring formulas that are true for each domain D ant] as- signment in D that satisfy the axioms. A symbolic language is first established with an exactly specified syntax (thus, a class of formulas), and then an exactly cleaned concept of proofs (by starting with axioms, logical or mathematical, and applying rules of inference). We call the result a formal system. (The first-orcler predicate calculus as described above is a formal system with only logical axioms.) For Whiteheact and Russell, our confidence in the result- the deduction of mathematics within PM was to rest on our being convinced of the correctness of the logical principles embodied in their version of logic, inclusive of the theory of types, from which all the rest is cleducecI. Hilbert proposed to "formalize" one or another mathe- matical theory, and he hoped to continue with the whole bocly of mathematics up to some point short of encountering the paradoxes, in formal systems. Typically, the mathematics for- malizect will in part be ideal and thus not supported by our intuitions. Then he wanted to look at such a system from outside. The formal system, looking just at its structure (apart from the meanings or supposed meanings expressed by the symbols, which guide the practicing mathematician) is a system of finite objects: symbols (from an at most countably infinite collection), finite sequences of symbols (like those

.e KURT GODEL 151 constituting formulas), and finite sequences of finite se- quences of symbols (like those constituting proofs). So there is the possibility of applying to the study of a formal system intuitive methods of reasoning in the real part of mathemat- ics (using only potential infinities), which Hilbert callecl (ni- tary (German Unit). In particular, Hilbert hoped by Unitary reasoning to prove the consistency of each of his formal systems, that is, that no two proofs in it can end in a pair of contradictory formulas A anct ,A. This would show that mathematics, as it has been cleveloped classically by adjoining the ideal statements to the real ones, is not getting into trouble. Thus Hilbert proposed to give a kind of justification to the cultivation of those parts of classical mathematics that the intuitionists reject. The mathematical discipline in which formal systems (often em- bodying ideal mathematics) are stucliecI from outside in re results. specs to their structure (leaving out of account the meanings of the symbols) as part of real mathematics, using only fini- tary methods, Hilbert caller! proof theory or metamathematics. Full-length expositions are in Hilbert and Bernays (1934, 1939) and Kleene (1952~. Now we are in a position to unclerstancl Godel's (1931a) Clearly, having embocliect some part of mathematics in a formal system, a question of completeness arises just as we saw for the formal system of the first-order predicate cal culus. Specifically, Gode} consiclerecT formal systems like that of Principia Mathematica and systems constructed! by the formal- ists that aim to formalize at least as much of mathematics as the elementary theory of the natural numbers. (A formal system that didn't do this much would be of rather little in- terest for the programs of the logicistic and formalistic schools.)

152 BIOGRAPHICAL MEMOIRS In such a system, propositions of elementary number theory can be expressed by closed formulas, that is, ones con- taining no free variables. Completeness should then mean that, for each closed formula A, either A itself or its negation, ~A, is provable. That is, for the system to be complete, proofs in the system shoul(1 provide the answer "yes" (A is provable) or "no" ~ MA is provable) to any question about natural numbers "Is the proposition P true?" such that P can be expressed, under the intended meaning of the symbols, by a closed formula A. For example, with the variables in teroreted to range over the natural numbers, if A(x,y) is a formula (with only the free variables x and y) expressing x By, one of the two closed formulas VxSyA(x,y) ant] ,VxSyA(x,y) should be true indeed the first is anct this one shouIct be provable if the formal system is complete. The open formulas 3xA(x,y) and , 3xA(x,y), in ordinary us- age, are synonymous with their closures lly3xA(x,y) and Sly ,3xA(x,y), anti neither is true. Godel's first incompleteness theorem of (1931a)-famous simply as "Godel's theorem"-says that a formal system S like that clescribed, if correct, is incomplete. There is in S a closed formula G such that, if in S only true formulas are provable, then neither G nor ,G is provable in S (although indeed under the intended interpretation G is trued. To be more specific about the assumption of correctness, let us take into account the form of G. which is VxA(x), where for the interpretation the intencled range of the variable x is the natural numbers. Here A(x) is a formula with the follow- ing property. Let us substitute in A(x) for the free occur- rences of the variable x successively the expressions (called numerals) O. O', O", ..., x, ... which express the natural numbers 0, I, 2, ..., x, .... ~ am (1enoting the numeral for x by "x", and ~ write the result of the substitution as "A(x)". For each x, one of A(x) ant! ,A(x) is provable. The assumption of cor

KURT GODEL 153 rectness that Gode} made is that for no formula A(x) and natural-number variable x are there proofs in S of all of A(O), A(~), A(2), ..., A(x), ... and also of ,VxA(x). This assumption he called m-consistency. (Simple) consistency is the property that for no formula A are there proofs of both of A and ,A. By applying m-consistency to \1xA, where x is a variable not oc- curring free in A, m-consistency implies simple consistency. Restating Godel's theorem with this terminology: If S is "-consistent, it is (simply) incomplete, that is, there is a closedformula G such that neither G nor ,G is provable in S (but G is true). How could this be? The fundamental fact is that in work- ing with a formal system (apart from its interpretation), the objects we are dealing with (the symbols from a finite or countably infinite collection, the finite sequences of (occur- rences) of those symbols, and the finite sequences of such finite sequences) form a countably infinite collection of lin- guistic objects. By pairing them one-to-one with the natural numbers, or using some other method of associating distinct natural numbers with them (as incleecl Gocle} dicI), each ob- ject of the formal system is represented by a number, now called its Gode! number. So indeecI, since the formal system S is adequate for a certain part of the elementary theory of the natural numbers, we can express in S propositions that by the Gode! numbers actually say things about the system S Itself. Now coded ingeniously constructed his G to be of the form b~xA(x), where A(x) expresses "x is not the Gode} num- ber of a proof of the formula with a certain fixed Gode} num- ber p" and p is the Gode} number of the formula G itself! Thus G says, "Every x is not the Gode! number of a proof of me", or simply "I am unprovable." So, if G were provable, G would be false. So (assuming correctness), G is unprovable; hence (by what G says) G is true; and hence (assuming cor- rectness) ,G is also unprovable. It is easy to confirm that m- consistency suffices as the correctness assumption in conclucI .

54 BIOGRAPHICAL MEMOIRS ing that ,G is unprovable, and simple consistency in con- cluding that G is Improvable. Goclel's formula G. which says "I am unprovable", is an adaptation of the ancient parallax of the liar. The Cretan Epi- menides (sixth century B.C.) iS reported to have said "Cretans are always liars." If this were the only thing Epimenides saicl, could it be true? Or false? To take the version of Eubulicles (fourth century B.C.), suppose a person says "The statement ~ am now making is false." If this statement is false, by what it says it would be true; and vice versa. Godel's substitution of"unprovable" for "false" escapes the paradox, because a statement and its negation can both be unprovable (while they cannot both be false). In two respects, Godel's theorem, as given in (1931a), has been improved. Rosser (1936), by using a slightly more com- plicated formula than Godel's G. replacecI Godel's hypothesis of m-consistency by the hypothesis of simple consistency. The other improvement, to be explainec! next, is connected with a clevelopment that took place essentially inclepenclently of Godel's (1931a) and is equally significant. At least since Euclid in the fourth century B.C., mathe- maticians have recognizes! that for some functions ant! precI- icates they have "algorithms". An algorithm is a procedure described in advance such that, whenever a value is chosen for the variable or a respective value for each of the variables of the function (or preclicate), the procedure will apply and enable one in finitely many steps to finct the corresponding value of the function (or to clecide the truth or falsity of the corresponding value of the predicate). In the 1930s, the general concept of an "algorithm" came uncler scrutiny, and Church in (1936) proposed his famous thesis ("Church's thesis" or "the Church-Turing thesis". This states that all the functions of natural number variables for which there are "algorithms", or which in Church's phrase

.. KURT GODEL 155 ology are "effectively calculable", belong to a certain class of such functions for which two equivalent exact descriptions had been formulates! during ~ 932-34. Turing in ~ ~ 937), in- clependently of Church, arrived at the same conclusion, using a third equivalent formulation, namely the functions computable by an idealized computing machine (error-free and with no bouncI on the quantity of its storage or "mem- ory") of a certain kind, now callecI a "Turing machine." The thesis applies to predicates, because a predicate can be rep- resented by the function taking O as its value when the value of the predicate is true and ~ when it is false. As Turing wrote (1937, 2301: "conclusions are reached which are superficially similar to those of Gode} tin ~ 193 balk." Gocle} ~ ~ 93 la) showocI the existence in certain formal systems S of"formally undecidable propositions", that is, proposi- tions for which the system S does not decide the truth or falsity by producing a proof of A or of- ~A, where A is the formula expressing the proposition in the symbolism of S. Church (1936) and Turing (1937) showed the existence of "intuitively undecidable predicates", that is, predicates for which there is no "decision procedure" or "effective process" or "algorithm" by which, for each choice of a value of its variable, we can decide whether the resulting proposition is true or false. In ~ ~ 936, ~ 943, ~ 952), I establishecI a connection between the two clevelopments. The fundamental purpose of using formal systems (as a refinement of the axiomatic-deductive method that has come clown to us from Pythagoras and Eu- clid in the sixth and fourth centuries B.C.) is to remove all uncertainty about what propositions hold in a given mathe- matical theory. For a formal system to serve this purpose, there must be an algorithm by which we can recognize when we have before us a proof in the system. Furthermore, for the system to serve as a formalization of a given theory, we

156 BIOGRAPHICAL MEMOIRS must have, for the propositions we are interested in, an al- gorithm to identify the formulas in the system that express those propositions. Of course, we can start with the formulas of the system, if they have an understood interpretation, and take as our class of propositions those expressed by the for- mulas. For the formalization of the theory of the natural numbers, using Gode} numberings of the formulas and proofs, the algorithms can be for number-theoretic functions and predicates, so the Church-Turing thesis can be appliecl. Gocle} established his theorem for "Principia Mathematica and related systems". In my generalize(1 versions of the theorem, ~ left out all the finer cletails of the formalization, and simply assumed that the purpose of formalization as de- scribecI above is servect, for the theory of the natural num- bers. Moreover, I chose in advance a fixed number-theoretic predicate P(a) so that every correct formal system fails to formalize its theory completely. Goclel's undeciciable propo- sitions in various formal systems are then all values of this one predicate. Thus: There is a predicate P(a) of elementary num- ber theory with the following property. Suppose that in a formal system S (i) there are formulas Aa for a = 0, I, 2, ... given by an algorithm (which formulas we take to express the propositions P(a) for a = 0, I, 2, ...) such that, for each a = 0, i, 2, ..., Aa is provable in S only if P(a) is true, and (ii) there is an algorithm for determining whether a given sequence offormulas in S is a proof in S of a given formula. Then there is a number p such that P(p) is true but Ap is un~rovahie in LS. If moreover (iii) there are formulas AN such that, for each a = 0, I, 2, · ~ ~ . Baa is provable in S only if P(a) is false. , ~\ , ~ then ,Ap is also unprovable in S (so Ap is undecidable in S). The predicate P(a) can be of a very simple form (sug- gested in Kleene (1936, Footnote 22), and used in his (1943, 19521: "for all x, Q(a,x)" where Q is a deciciable predicate. (A fuller exposition is in Kleene 1976, 768-69.) As I expressed the generalizecl Gocl~el theorem in a lecture

.. KURT GODEL 157 at the University of Wisconsin in the fall of 1935 (with my (1936) already written, and knowing the contents of Church ~ ~ 936) but not yet of Turing ~ 19374), the theory of the natural numbers indeed just the theory of the limited part of it represented by the predicate P(a)-offers inexhaustible scope for mathematical ingenuity. No one will ever succeecI in writing down explicitly a list of principles (given as a formal system) sufficient for providing a proof of each of the prop- ositions P(a) for a = 0, I, 2, ... that is true. To recapitulate, by Godel's first incompleteness theorem, as he gave it in (1931a), none of the familiar formal systems (like that of Principia Mathematical, and by the generalizecT version of the theorem, which Gocle! accepted in a "Note adclect 28 August 1963" to the van Heijenoort (1967) trans- lation of his (1931a) anc! in the "Postscriptum" to the Davis (1965) reprint of his (1934), no conceivable formal system, can be both correct and complete for the elementary theory of the natural numbers. In Goclel's first incompleteness theorem (as stated above for Principia Mathematica ant] relatecI systems), the unprova- bility of G follows from the assumption that S is simply con- sistent. By Godel's numbering, the property of the simple consistency of S can be expressed in S itself by a formula, call it "Consis". And in fact the reasoning by which Gocle! showed that "Simple consistency implies G is unprovable" can be for- malized within S as a proof of the formula Consis ~ G. noting that G says "G is unprovable"! Therefore, if Consis were provable in S. by one application of the rule of inference shown first above, G wouIc] be, contradicting Goclel's first in- completeness theorem if S is consistent. So we have Godel's second incompleteness theorem of (1931a): If S is simply con- sistent, the formula Consis expressing that fact is unprovable in S. Hilbert's iclea hac! been to prove the consistency of a suit

158 BIOGRAPHICAL MEMOIRS able formal system S of mathematics by Unitary methods. In the interesting case that S is a formalization embracing some ideal (non-finitary) mathematics, the methods to be used in proving its consistency should not inclucle all those formal- izec! in S. Godel's second theorem shows that not even all the methods formalizes! in S would suffice! The consequence is that, if Hilbert's idea can be carried out, it cannot be done as simply as presumably hac! been hoped. Methods will have to be accepted as Unitary, and used in the consistency proof of a system S. that are not formal- izable in S. Incleed, this has now been done for the arithmetic of the natural numbers by Gentzen ~ ~ 936), Ackermann (1940), and Gode! (195Sa), and for analysis (real-number theory) by Spector (1961), extending Go(le! (195Sa). With the two incompleteness theorems of Gode} (1931a), the whole aspect of work on the foundations of mathematics was profouncIly altered. We have clescribed Godel's celebrated results in (1930a) and (1931a) in the context of the outlook on foundations at the time. He clearly acIdressect ant! solved problems ex- isting at that time. Each of these results can be construed as a piece of exact mathematics: on the level of classical number theory in the case of (1930a), and of Unitary number-theory in the case of ( 193 la). The picture mathematicians could en- tertain of the possibilities for the use of formal systems has been refocused by Goclel's discoveries. Now we know that their use cannot give a resolution of the foundational prob- lems of mathematics as simply as hac} been hoped. But, in my view, formal systems will not go away as a concern of math- ematicians. Recourse to the axiomatic-decluctive method, as refines! in modern times to formal systems, provides mathe- maticians with the means of being fully explicit about what they are doing, about exactly what assumptions they have used in a given theory. It is important to have this explicitness

.. KURT GODEL 159 when they are engaged in conceiving new methods (as Go- clel's first (193la3 theorem shows that for progress they must) and attempting to assure themselves of their soundness (which by Godel's second theorem cannot be done simply by the metamathematical applications of only the same methods). In the period we are reviewing (after (1930a) and prior to 193Xa)), Gode} made a number of other significant con . . try Buttons. In (1934), building on a suggestion of Herbrand (see van Heijenoort (1967, 6191), he introduced the notion of"gen- eral recursive functions", which ~ studied in (19361. This is one of the two equivalent notions that were identified with "effective calculability" by Church's thesis mentioned above. Nevertheless, Gode} clid not accept the thesis until later (Kleene 1981, 59-621. Concerning those notions and the third one of Turing, and generalizations of them, a very extensive mathematical theory has been developed (with an important role played by the Herbrand-Gode} notion) and applied to other branches of mathematics (Kleene (19X1, 62-64~. In ~ 193 I by, Gocle} explained how some of his undecidable propositions become decidable with the addition of higher types of variables, while of course other undecidable propo- sitions can be described. In a trenchant paper (1935), he showed that in the systems with higher types of variables in- finitely many of the previously provable formulas acquire very much shorter proofs. He also o~erect contributions to the so-called Entscheidungsproblem (decision problem) for the first-order predicate logic (1930f, 1933b). This is the prob- lem of finding an algorithm, at least for a described class of formulas, for deciding whether a formula is or is not prov- able. ~ 193 Ic) is historic as one of the first results on a "formal system" with uncountably many symbols.

160 BIOGRAPHICAL MEMOIRS The intuitionistic school under Brouwer came to recog- nize the advantages of formalization for making explicit the boundaries of a given body of theory. So Heyting in (1930a, 1930b) gave a formalization of the intuitionistic logic and of a portion of the intuitionistic mathematics. This has had various mathematical applications. Goclel's papers ~ ~ 932c, 1932d, 1932e) were important contributions to the stucly of these systems. The article of Smorynski and that of Paris ant! Harring ton in Barwise (1977), and Dawson (1979), can serve as a sampling of the reverberations after nearly fifty years from Godel's ~ ~ 93 ~ a) incompleteness theorems. GODEL S RELATIVE CONSISTENCY PROOF FOR THE AXIOM OF CHOICE AND FOR THE GENERALIZED CONTINUUM HYPOTHESIS (Rosa, Sub, ~sssa, ~sssby As remarked above, in Cantor's set theory, the set of the sets of natural numbers, ant! the set of the real numbers, have a cardinal number To greater than the cardinal number R0 of the set of the natural numbers, which is the least infinite cardinal. In Cantor's theory, the cardinal number it, next greater than R0 is identified as the cardinal of the set of all possible linear orderings of the natural numbers in which each sub- set of them has a first member in the ordering ("well- or(lerings"~. Cantor's set theory would be greatly simplified if To, which is the infinite cardinal greater than R0 coming to mine] first, is actually the next greater cardinal. Cantor con- jecturect in (1878) that it is, that To = Hi. This conjecture is called the "continuum hypothesis" (CH); ant! it became the central problem of set theory to confirm or refute CH. Sixty years later, with the problem still unsolved, Goclel's results in ~ 10.~ 1 9.~Rh. 10.~. 1 9.39b) put the matter in a new light.

.. KURT GODEL . 161 Using Cantor's ordinal numbers, all the infinite cardinals can be listed in order of magnitude as ~o, ~, ~2' ·~' ~, ·~e ~ where ~ ranges over the natural numbers as finite ordinals, and then on into Cantor's infinite ("transfinite") ordinals. The "generalized continuum hypothesis" (GCH) is that, for each orclinal a, 2X~ = HO`+, where 2X~ is the carclinal of the set of all the subsets of a set of cardinal NO`. The theory of sets was axiomatized after the paradoxes had appeared. This consisted in listing a collection of axioms, regarcle(1 as true propositions about sets, including axioms providing for the existence of many sets but not of too "wilcI" sets such as hac! given rise to the paradoxes. (We recall the Skolem paradox about such systems of axioms in first-order logic.) As a standard list of axioms for set theory, ~ will take those commonly called the Zermelo-Fracnke! axioms. These arise from the first axiomatization by Zermelo in (1908) by using a refinement proposed by Fracnke} in (19224. One of the axioms, called the "axiom of choice" (AC), has been re- garclect as less natural than the others. One form of it says that, if we have a collection S of non-empty sets, no two of which have a member in common, there is a "choice set" C containing exactly one member from each set in the collec- tion S. By ZFC ~ shall mean all the Zermelo-Fracnke! axioms, and by ZF the system of those axioms without AC. Cantor had not been thinking of his conjecture that To = H~ (CH) relative to a set of axioms. But after choosing an axiomatization, say ZF, there are three possibilities: (~) To = R~ is provable (using elementary logic) from the axioms. (2) '(2~o = H~) is provable from the axioms. (3) Neither (~) nor (21. This is assuming the axioms are consistent, so that not: (4) Both (~) and (21. What Gocle} clid was to exclude (2~; he showed that adcling

162 BIOGRAPHICAL MEMOIRS Ho = R~ to the axioms will not leacI to a contradiction (if a contradiction is not already declucible from the axioms with- out the additions. To put the matter in its simplest terms, Godel, using only things about sets justified by the axioms ZF, defined a class L of sets, which he called the "constructible sets", such that all the axioms are true when the "sets" for them are taken to be just the constructible sets L. In effect, L constitutes a kind of skeletal mocle} of set theory-not all the sets presumably in- tencled, but still enough to make all the axioms true. Ant! in this model, AC ant] CH, ant! indeecI GCH, are all true. Since nothing is used about sets in this reasoning with L that cannot be based on the axioms ZF, it can be converted as follows into a demonstration that if ZF (taken as the formal system with the mathematical axioms of ZF anct the logical axioms and rules of inference of the first-order predicate calculus) is (simply) consistent, so is ZF + AC + GCH (sim- ilarly taken). Suppose ZF is consistent, and (contrary to what we want to prove) that a pair of contradictory formulas A ant! ,A (which we can take to be closecI) are provable in ZF + AC + GCH. Let Be come from any closed formula B by replacing each part of the form VxC by VxfxeL ~ C) and each part of the form 3xC by SxfxeL & C), in effect restrict- ing the variable x to range over L. Here xeL is definable within ZF. Now for the axioms Ao' A,, A2, ... of ZF + AC + GCH, we can prove in ZF At' At, At, ..., and then continue by the reasoning that gave the contradiction A ant! MA in ZF + AC + GCH to get the contradiction At and FAT in ZF, contradicting our supposition that ZF is consistent. Thus Gocle} gave a consistency proof for ZF + AC + GCH relative to ZF. It is natural to ask whether one can also rule out Ail, that is, whether the negation Ho = H~ of the continuum hy

.. KURT GODEL 163 pothesis can be adcled consistently to ZF or indeeci to ZFC (provided ZF is consistent). It remained for Paul Cohen in (1963, 1964) to clo this. He accomplished this by using an- other mocle! (quite different from Godel's) in which all the axioms of ZFC and also Go = R~ hold. (For a comment by Godel, see 1967.) Thus, combining Godel's and Cohen's results, Go = S~ is independent of ZFC. Similarly, combining results of Gode} and Cohen, AC is independent of ZF. These results of Gocle! and Cohen have ushered in a whole new era of set theory, in which a host of problems of the consistency or inclependence of various conjectures relative to this or that set of axioms are being investigated by constructing moclels. PRINCETON (IAS) 1939-1978 After Godel's return to Princeton in 1939, he never again left the United States. He became a U.S. citizen in 1948. He received annual visiting appointments from the Institute for Advanced Stucly from 1940-41 on, became a permanent member in 1947, a professor (in the School of Mathematics) in 1953, ant! retiree! in 1976. He was keenly interested in the affairs of the Institute, and conscientious in work for the In- stitute, especially in the evaluation of applicants. ~ have already reviewed most of his work that was pub- lished in his own papers. The last paper of his in the Bibli- ography (195Sa), mentioned above, gives a new interpreta- tion of intuitionistic number theory, which Wang (1981, 657) says "was obtained in 1942. Shortly afterwards he lecturer! on these results at Princeton and Yale." Goclel's (1944, 1947) are exceedingly suggestive expository and critical articles on Russell's mathematical logic and on the continuum problem. In December ~ 946, Gocle! presented a paper to the Princeton Bicentennial Conference on Problems of Mathe

64 BIOGRAPHICAL MEMOIRS matics, published in 1965, suggesting a non-constructive ex- tension of formal systems, or of the notion of "clemonstra- bility", to be obtained by using stronger and stronger "axioms of infinity" asserting the existence of large carclinal numbers in set theory. He wrote, "It is not impossible that for such a concept of demonstrability some completeness theorem would hoist which would say that every proposition expres- sible in set theory is cleciclable from the present axioms plus some true assertion about the largeness of the universe of all sets." The paper makes a similar suggestion regarding the concept of mathematical "definability". Gove! and Einstein, both at the Institute for AdvancecI Study, saw much of each other. Because of Godel's interest in Kant's philosophy of space and time, Godel became inter- estec] in general relativity theory, on which he workoct cluring ~ 947 to ~ 950 or ~ 95 ~ . Three short articles ~ ~ 949a, ~ 949b, 1950) resultecI. According to R. Penrose, as reported in Krei- se} (1980, 214-15), "Lthese articles] were highly original and, in the long run, quite influential.....Goclel's work served as a cross check on mathematical conjectures and proofs in the modern global theory of relativity." (For summaries, see Krei- se! loc. cit. and Dawson 1983,266-67, the Hacienda and Cor- rigenda to which reports on a controversy about it.) Gode! was deeply interested in philosophy, and in the rel- evance of philosophical views to the mathematical problems with which his work dealt. Wang writes (1981, Footnote 9), "we may conjecture that between 1943 and 1947 a transition occurred from Goclel's concentration on mathematical logic to other theoretical interests which are primarily philosoph- ical.... From this papers (1946, 1947~] one gets the clear impression that Gode} was interested only in really basic ad- vances." Kreise} (1980, 204-13) calls Goclel's first proposal in (1946) "Goclel's programme", and discusses it while citing

.. KURT GODEL 165 Kanamori and Magidor (19~77) for more complete references to the work done on the program over the last thirty-five years. According to Wang (1978, 183; 1981,658), Godel worked on several papers (as early as 1947, perhaps), which in the end he did not publish. One of these was his Josiah Willard Gibbs Lecture, Some Basic Theorems on the Foundations of Math- ematics and their Philosophical Implications, which he read from a manuscript to the American Mathematical Society on De- cember 26, 1951 (} was present). Some of the ideas in this lecture are reported by Wang in the pages cited as Gode} (1974a). Gode! left a considerable quantity of notes (almost 5,000 pages, according to Kreise! 1980, 1511. Undoubtedly, these will constitute a mine for scholars for quite some time into the future. Gode} contributed reflections on some of his papers as emendations, amplifications, and additions to reprints and translations (see Bibliography, 1939, 1946, 1949b, 1963- 66a). Gode} was rather retiring. But he was kind and responsive to qualified interlocutors who took the initiative to engage him in discussions. So it has come about that various reflec- tions and views of his have been reported with his permission in writings by other authors. Also, on occasions, he took the initiative to volunteer pronouncements other than in papers of the usual sort. ~ have included in this Bibliography all the material of these two kinds that has come to my attention (without attempting to draw a line between the substantial, and the slight). This accounts for ~ 193 id) and all of the items after (1950), except (1958a) and (1963-66a). On the occasion of the award of an Einstein Medal to Gode! on March 14, 1951, John van Neumann began his tribute to Gode} (von Neumann 1951) with the words:

166 BIOGRAPHICAL MEMOIRS Kurt Godel's achievement in modern logic is singular and monumen- tal-indeed it is more than a monument, it is a landmark which will remain visible far in space and time. REFERENCES Ackermann, W. 1940. Zur Widerspruchsfreiheit der Zahlentheo- rie. Math. Ann., 1 17: 162-94. Agazzi, E. 1961. Introdazione al Problemi dell'Assiomatica. Milan: So- cieta Editrice Vita e Pensiero (Pubblicazioni dell'Universita Cat- tolica del Sacro Cuore Ser. III. Scienze Filosofiche, 4~. Barwise, I., ed. 1977. Handbook of Mathematical Logic. Amsterdam, New York, and Oxford: North-Holland. Benacerraf, P. and H. Putnam, eds. 1964. Philosophy of Mathematics: Selected Readings. Englewood Cliffs, N. J.: Prentice-Hall. Berka, K. and L. Kreiser, eds. 1971. Logik-Texte. Berlin: Akademie- Verlag. Brouwer, L. E. I. 1908. De onbetrouwbaarheid der logische prin- cipes. Tijdsch. voorwijsbegeerte, 2:152-58. Bulloff, I. }., T. C. Holyoke, and S. W. Hahn, eds. 1969. Foundations of Mathematics, Symposium Lof April 22, 1966] Papers Commemo- rating the Sixtieth Birthday of Kurt Godel. New York, Heidelberg, and Berlin: Springer. Cagnoni, D., ed. 1981. Teoria delta dimostrazioni. Milan: Feltrinelli. Cantor, G.1874. Uber eine Eigenschaft des Inbegriffes alter reellen algebraischen Zahlen. four. reine angew. Math., 77:258-62. Cantor, G. 1878. Ein Beitrag zur Mannigfaltigkeitslehre. foux reine angew. Math., 84: 242-58. Cantor, G. 1895, 1897. Beitrage zur Begrundung der transfiniten Mengenlehre. Erster Artikel, Math. Ann., 46:481-512; Zweiter Artikel, 49:207-46. Casari, E. 1973. La Filosopa delta Matematica del 1900. Florence: ~ . Kansans. Church, A. 1936. An unsolvable problem of elementary number theory. Am. /! Math., 58:345 -63. Cohen, P. 1963, 1964. The independence of the continuum hy- pothesis. I. Proc. Natl. A cad. Sci. USA, 50:1143-48; II. 51:105- 10. Davis, M., ed. 1965. The Undecidable. Basic Papers on Undecidable

.. KURT GODEL 167 Propositions, Unsolvable Problems and Computable Functions. Hew- lett, N.Y.: Raven Press. Dawson, J. W., Jr. 1979. The Godel incompleteness theorems from a length-of-proof perspective. Am. Math. Mon., 86:740-47. Dawson, t. W., Jr. 1983. The published work of Kurt Godel: An annotated bibliography. Notre Dame f. Formal Logic, 24:255-84. Addenda and Corrigenda, 25:283-87. Felgner, U., ed. 1979. Mengenlehre (Wege der Forschung). Darm- stadt: Wissenschaftliche Buchgesellschaft. Fracnkel, A. 1922. Der begriE"definit" und die Unabhangigkeit des Auswahlaxioms. Sitz. Preuss. Akad. Wiss., Phys.-math. Kl., 1922:253-57. Frege, G. 1879. Begri~sschrift, eine der arithmetische nachgebildete For- melsprache des reinen Denkens. Halle: Nebert. Gentzen, G. 1936. Die Widerspruchsfreiheit der reinen Zahlen- theorie. Math. Ann., 112:493 -565. Goldfarb, W. D. 1981. On the Godel class with identity. i. Symb. Logic, 46:354-64. Grattan-Guinness, I. 1979. In memoriam Kurt Godel: His 1931 correspondence with Zermelo on his incompletability theorem. Hist. Math., 6:294 - 304. Greenberg, M. T 1980. Euclidean and Non-Euclidean Geometries, De- velopment and History, 2d. ed. San Francisco: Freeman. Henkin, L. 1947. The Completeness of Formal Systems. Ph.D. thesis, Princeton University. Heyting, A. 1930a. Die formalen Regeln der intuitionistischen Lo- gik. Sitz. Preuss. Akad. Wiss., Phys.-math. Kl., 1930: 42-56. Heyting, A. 1930b. Die formalen Regeln der intuitionistischen Mathematik. Sitz. Preuss. Akad. Wiss., Phys.-math. Kl., 1930: 51- 71, 158-69. Heyting, A. 1971. Intuitionism. An Introduction. 3d rev. ed. Amster- dam: North-Holland. .. Hilbert, D. 1904. Uber die Grundlagen der Logik und der Arith- metik. In: Verh. 3. Internat. Math.-Kong. in Heidelberg 8-13 Aug. 1904, pp. 174-85. Leipzig: Tuebner, 1905. Hilbert, D. and W. Ackermann. 1928. Grundzage der theoretischen Logik. Berlin: Springer. Hilbert, D. and P. Bernays. 1934, 1939. Grundlagen der Mathematik. 2 vols. Berlin: Springer.

68 BIOGRAPHICAL MEMOIRS Kanamori, A. and M. Magidor. 1978. The evolution of large car- dinal axioms in set theory. In: Higher Set Theory, Proceedings, Oberwolfach, Germany, April 13-23, 1977, ed. G. H. Muller and D. S. Scott, pp. 99-275. Berlin, New York: Sorinaer (Lecture Notes in Mathematics, 669~. Kleene, S. C. 1936. General recursive functions of natural num- bers. Math. Ann., 1 12: 727-42. Kleene? S. C. 1943. Recursive predicates and quantifiers. Trans. Am. Math. Soc., 53:41-73. Kleene, S. C. 1952. Introduction to Metamathematics. Amsterdam: North-Holland. (Eighth reprint, 1980.) Kleene, S. C. 1976, 1978. The work of Kurt Godel.). Symb. Logic, 41 :761-78; An Addendum, 43:613. Kleene, S. C. 1981. Origins of recursive function theory. Ann. Hist. Comp., 3:52-67. (after p. 52 rt. colt 1. 5 add "thefirst of"; be- fore p. 59 it. colt 1. 4 from below, add "in 1934"; p. 60 it. colt 1. 17, remove the reference to Church; p. 63 It. colt 1. 4 from below, for "1944" read "1954"; p. 64 It. colt bottom 1., for "do" read"l`°".) Klibansky, R., ed. 1968. Contemporary Philosophy, A Survey, I, Logic and Foundations of Mathematics. Florence: La Nuova Italia Edi- tr~ce. 1 a Kreisel, G. 1958. Elementary completeness properties of intuition- istic logic with a note on negations of prenex formulas. ). Symb. Logic,23:317-30. Kreisel, G. 1962. On weak completeness of intuitionistic predicate logic. l. Symb. Logic, 27:139-58. Kreisel, G. 1980. Kurt Godel, 28 April 1906-14 January 1978. Biogx Mem. Fellows R. Soc., 26:148-224. Corrigenda, 27:697; 28:718. Louren~o, M., ed. and trans. 1979. O teorema de Godel e a hipotese do continua. Lisbon: Fundacsao Calouste Gulbenkian. Lowenheim, L. 1915. Uber Moglichkeiten im Relativkalkul. Math. Ann., 76:447 - 70. Moster~n, I., ed. 1981. Kurt Godel, Obras Completas. Madrid: Alianza Editorial. Parvu, I., ed. 1974. Epistemologie. Orientari Contemporane. Bucarest: Editura Political Pears, D. F., ed. 1972. Bertrand Russell, A Collection of Critical Essays. Garden City, N.Y.: Anchor Books.

.. KURT GODEL 169 Quine, W. V. 1978. Kurt Godel ~ 1906 -19781. Year Book Am. Philos. Soc.: 81-84. (On p. 84, for "John von Neumann" read "Julian Schwinger".) Rautenberg, W. 1968. Die Unabhangigkeit der Kontinuumhy- pothese Problematik und Diskussion. Math. in der Schule, 6:18-37. Reinhardt, W. N. 1974. Remarks on reflection principles, large car- dinals, and elementary embeddings. In: Axiomatic Set Theory; Proc. Symposia Pure Math., XIII ~ July 10-August 5, 1967), Part II, ed. T. J. Jech, pp. 187-205. Providence, R.I.: American Mathematical Society. Robinson, A. 1974. Non-Standard Analysis, 2d ed. Amsterdam: North-Holland. Rosser, I. B. 1936. Extensions of some theorems of Godel and Church. ). Symb. Logic, 1: 87-91. Russell, B. 1908. Mathematical logic as based on the theory of types. Am. J. Math., 30:222-262. Saracino, D. H. and V. B. Weispfennig, eds. 1975. Model Theory and Algebra. A Memorial Tribute to Abraham Robinson. Berlin, Heidel- berg, and New York: Springer (Lecture Notes in Mathematics, 498~. Schilpp, P. A., ed. 1944. The Philosophy of Bertrand Russell. Evanston and Chicago, Ill.: Northwestern University Press. Schilpp, P. A., ed. 1949. Albert Einstein, Philosopher-Scientist. Evans- ton, Ill.: Northwestern University Press. (German edition, Albert Einstein als Philosoph und Naturforscher. 1955. Stuttgart: Kohl- hammer.) Skolem, T. 1920. Logisch-kombinatorische Untersuchungen uber die Erfullbarkeit oder Beweisbarkeit mathematischer Satze nebst einem Theoreme uber dictate Mengen. Skrifter utgit av Videnskapsselskapet i Kristiania, I. Matematisk-naturvidenskabelig klasse 1920, no. 4. Skolem, T. 1923. Einige Bemerkungen zur axiomatischen Be- grundung der Mengenlehre. In: Wissenschaftliche Vortrage 5. Kong. Skand. Math. Helsingfors 4-7 [uli 1922. Helsin~fors. on. 217-32. Skolem, T. 1933. Uber die Unmoglichkeit einer vollstandigen Charakterisierung der Zahlenreihe mittels eines endlichen Ax- iomensystems. Norsk matematisk forenings skrifter, ser. 2, no. 10: 73-82. - ~ - -' 1 1

170 BIOGRAPHICAL MEMOIRS Skolem, T. 1934. Uber die Nicht-charakterisierbarkeit der Zahlen- reihe mittels endlich oder abzahlbar unendlich vieler Aussagen mit ausschliesslich Zahlenvariablen. Fund. Math., 23: 150-61. Spector, C. 1962. Provably recursive functionals of analysis: A con- sistency proof of analysis by an extension of principles formu- lated in current intuitionistic mathematics. In: Recursive Func- tion Theory; Proc. Symposia Pure Math., V (Abril 6-7, 1961J, ed. I. C. E. Dekker, pp. 1-27. Providence, K.1.: American Mathe- matical Society. (Posthumous, with footnotes and some editing ~-r--~~~ - ~~~ ~ -- - ~~~~~~, \ 1 by Kreisel and a postscript by Godel.) Turing, A. M. 1937. On computable numbers, with an application to the Entscheidungsproblem. Proc. London Math. Soc., ser. 2, 42:230-65. (A correction, 43:544-46.) Ulam, S. 1958. John von Neumann, 1903-1957. Bull. Am. Math. Soc., 64, no. 3, pt. 2: 1 - 49. van Heijenoort, I., ed. 1967. From Frege to Godel: a Source Book in Mathematical Logic, 1879-1931. Cambridge, Mass.: Harvard University Press. (The English translations Land introductory notes thereto] of Godel ~ 1930e, 1931 a, 1931 b) and of Frege ~ 1879) in this volume are reprinted in Frege and Godel: Two Fun- damental Texts in Mathematical Logic, 1970.) van Neumann, I. 1927. Zur Hilbertschen Beweistheorie. Math. Zeit., 26:1-46. von Neumann, l. 1951. ETribute to Kurt Godel quoted in] The New York Times, March 15, 1951, 31. BulloE et al., 1 969. ~ , ,, · · %, . ~ (More fully on pp. (ix)-(x) of von Neumann, I. 1966. Theory of Self-Reproducing Automata (post- humous), ed. and completed by A. W. Burks. Urbana and Lon- don: University of Illinois Press. Wang, H. 1974. From Mathematics to Philosophy. London: Routledge & Kegan Paul; New York: Humanities Press. Wang, H. 1978. Kurt Godel's intellectual development. Math. Intel- ligencer, 1:182 - 84. Wang, H. 1981. Some facts about Kurt Godel. [. Symb. Logic, 46:653-59. Whitehead, A. N. and B. Russell. 1910, 1912, 1913. Principia Math- ematica. 3 vols. Cambridge, U.K.: Cambridge University Press. Zermelo, E. 1908. Untersuchungen uber die Grundlagen der Men- genlehre I . Math. Ann., 65:261-81.

.. KU RT G O D E L HONORS AND DISTINCTIONS AWARDS AND MEMBERSHIPS 171 Albert Einstein Award, Lewis and Rosa Strauss Memorial Fund (shared with Julian Schwinger), 1951 National Academy of Sciences, Member, 1955 American Academy of Arts and Sciences, Fellow, 1957 American Philosophical Society, Member, 1961 London Mathematical Society, Honorary Member, 1967 Royal Society (London), Foreign Member, 1968 British Academy, Corresponding Fellow, 1972 Institut de France, Corresponding Member, 1972 Academic des Sciences Morales et Politiques, Corresponding Mem- ber, 1972 National Medal of Science, 1975 HONORARY DEGREES D.Litt., Yale University, 1951 Sc.D., Harvard University, 1952 Sc.D., Amherst College, 1967 Sc.V., Rockefeller University, 1972

172 BIOGRAPHICAL MEMOIRS ANNOTATED BIBLIOGRAPHY I have listed the original items in the order of their authorship by Godel, insofar as I could find information to base this on. Thus 1939b, commu- nicated by Godel on February 14, 1939, is put after 1939a, which is a set of notes by George W. Brown published in 1940 on lectures delivered by Godel in the fall term of 1938-39; and 1934 and 1946, only published in 1965, are in the right order. This has involved using dates of presentation for the eleven items listed from Ergebnisse eines mathematischen Kolloquiums (ea. Karl Menger). Not listed are four brief contributions by Godel to dis- cussions in these Ergebnisse (4:4, 4:6, 4:34~51), 7:6), twenty-seven reviews by Godel in Zentralblatt fur Mathematik und ihrer Grenzgebiete 1931-36, six reviews by Godel in MonatsheftefurMathematik und Physik 1931-33, and the Spanish translations in Moster~n (1981) of all of the papers of Godel ex- cept 1932a, 1932b, and 1933a. (In Dawson (1983), the four Ergebuisse items are cited (just before F1933a] and as t1933], t1933d1, f 19364), as well as the twenty-seven Zentralblatt reviews and the Moster~n (1981) transla- tions, while the six Monatshefte reviews are cited in its Addenda and Cor- rigenda.) The other translations and reprintings of Godel's papers are cited within the items for the originals. Eight of the translations (with no inputs by Godel, as far as I know) are thus cited concisely through their reviews or listings in the journal of Symbolic Logic. Books (not journals) are generally cited through the Reference section. For example, the English translation of 1930a is on pp. 583-91 of the book listed in the References as "van Heijenoort, l., ed. 1967." A work entitled Kurt Godel, Sein Leben und Wirken, W. Schimanovich and P. Weibel, eds., is to be published by Verlag Holder-Pichler-Tempsky, Vi- enna. It will contain some of Godel's works and various biographical and . . uterpretatlve essays. The Association for Symbolic Logic is arranging for the publication in the original (by Oxford University Press, ed. by S. Feferman et al.), and when the original is in German also in English translation, of all of Godel's pub- lished works, with introductory historical notes to them and a biographical introduction and survey. (Volume I ~ 1986) contains Godel's published works up through 1936; the rest will be in Volume II, probably ir~ 1986. A further volume or volumes are projected to contain a selection of un- published material from Godel's Nachlass.) 1930 a. Die Vollstandigkeit der Axiome des logischen Funktionenkalk uls. Monatsh. Math. Phys., 37:349-60. (English bans: van Hei- jenoort, 1967, pp. 583-91, with two comments by Godel, pp.

.e KURT GODEL 173 510-11; also see Kleene, 1978; reprinted in: Berka and Kreiser, 1971, pp. 283-94.) b. Uber die Vollstandigkeit des Logikkalkuls (talk of 6 Sept. 1930~. Die Naturwissenschaften, 18: 1068. c. FRemarks in] Diskussion zur Grundlegung der Mathematik F7 Sept. 19301. Erkenntnis (1931), 2:147-48. d. Nachtrag Lto the preceding remarks1. Erkenntnis, 2:149-51. (Italian bans: Casari, 1973, pp. 55-57.) e. Einige metamathematische Resultate uber Entscheidungsdefin- itheit und Widerspruchsfreiheit. Anz. Akad. Wiss. Wien, Math.- naturwiss. K1. 67:214-15. (English trans.: van Heijenoort, 1967, pp. 595-96; reprinted in: Berka and Kreiser, 1971, pp. 320- 21.) f. Ein Spezialfall des Entscheidungsproblems der theoretischen Logik. Ergeb. math. Kolloq. (for 1929-30, publ. 1932), 2:27- 28. 1931 a. Uber formal unentscheidbare Satze der Principia Mathematica und verwandter Systeme I. Monatsh. Math. Phys., 38:173-98. (English trans., 1962, see J. Symb. Logic, 30:359-62; also in: Davis, 1965, pp. 5-38 (see J. Symb. Logic, 31:486-891; with a note by Godel, in: van Heijenoort, 1967, pp. 596-616. Italian trans.: Agazzi, 1961, pp. 203-28; Portuguese trans.: Lourenc,o, 1979, pp. 245-90.) b. Uber Vollstandigkeit und Widerspruchsfreiheit. Ergeb. math. Kolloq. (for 22 Jan. 1931, publ. 1932), 3: 12-13. (English trans., with a remark by Godel added to Ftn. 1: van Heijenoort, 1967, pp. 616-17.) c. Eine Eigenschaft der Realisierung des Aussagenkalkuls. Ergeb. math. Kolloq. (for 24 Tune 1931, publ. 1932), 3:20-21. d. Letter to Zermelo, October 12, 1931. In: Grattan-Guinness, 1979, pp. 294-304. Uber Unabhangigkeitsbeweise im Aussagenkalkul. Ergeb. math. Kolloq. (for 2 Dec. 1931, publ. 1933), 4:9-10. 1932 . . a. Uber die metrische Einbettbarkeit der Quadrupel des R3 in Ku- gelflachen. Ergeb. math. Kolloq. (for 18 Feb. 1932, publ. 1933), 4: 16-17.

174 BIOGRAPHICAL MEMOIRS b. Uber die Waldsche Axiomatik des Zwischenbegriffes. Ergeb. math. Kolloq. (for 18 Feb. 1932, publ. 1933), 4:17-18. c. Zum intuitionistischen Aussagenkalkul. Anz. Akad. Wiss. Wien, Math.-naturwiss. K1. (for 25 Feb. 1932), 69:65-66. (Reprinted, with an opening clause attributing the question to Hahn, in Ergeb. math. Kolloq. (for 1931-32, publ. 1933), 4:40; and in Berka and Kreiser, 1971, p. 186.) d. Zur intuitionistischen Arithmetik und Zahlentheorie. Ergeb. math. Kolloq. (for 28 June 1932, publ.1933),4:34-38. (English trans.: Davis, 1965, pp. 75-81 (see i. Symb. Logic, 31:490-911. Portuguese trans.: Louren~o, 1 979, pp. 359-69.) Fine Interpretation des intuitionistischen Aussagenkalkuls. Er- geb. math. Kolloq. (for 1931-32, publ.1934), 4:39-40. (English trans., 1969, see J. Symb. Logic, 40:498; reprinted in: Berka and Kreiser, 1971, pp. 187-88~. I. Bemerkung uber projektive Abbildungen. Ergeb. math. Kolloq. (for 10 Nov. 1932, publ. 1934), 5: 1. 1933 a. With K. Menger and A. Wald. Diskussion uber koordinatenlose Differentialgeometrie. Ergeb. math. Kolloq. (for 17 May 1933, publ. 1934), 5:25 -26. Zum Entscheidungsproblem des logischen Funktionenkalkuls. Monatsh. Math. Phys. (received 22 June 1933),40:433-43. (For a correction, see Goldfarb, 1981.) 1934 On Undecidable Propositions of Formal Mathematical Systems. Mimeo- graphed notes by S. C. Kleene and J. B. Rosser on lectures at the Institute for Advanced Study, Feb.-May, 1934, 30 pp. (Ex- tensively distributed, deposited in some libraries, and listed in the }. Symb. Logic Bibliography 1:206; printed with correc- tions, emendations, and a Postscriptum, by Godel in Davis 1965, pp. 41-74 (see J. Symb. Logic, 31:489-90~. A relevant Godel letter of 15 Feb. 1965 is quoted there on p. 40, and in Kleene, 1981, pp. 60, 62, and of 23 April 1963 in van Heijenoort 1967, p. 619. Portuguese trans. in Louren~o 1979, pp. 291-358.) 1935 Uber die Lange von Beweisen. Ergeb. math. Kolloq. (for l9 June 1935, with a remark added in the printing 1936),7:23-24. (En

.. KURT GODEL 175 glish trans.: Davis 1965, pp. 82-83 (see d. Symb. Logic. 31:491). Portuguese trans.: Lourenc,o 1979, pp. 371-75. 1938 a. The consistency of the axiom of choice and of the generalized continuum-hypothesis. Proc. Natl. Acad. Sci. USA (communi- cated 9 Nov. 1938), 24:556 -57. b. The consistency of the generalized continuum-hypothesis. Bull. Am. Math. Soc. (abstract of a talk on 28 Dec. 1938, publ. 1939), 45:93. 1939 a. The Consistency of the Axiom of Choice and of the Generalized Contin- uum-Hypothesis with the Axioms of Set Theory. Notes by G. W. Brown on lectures at the Institute for Advanced Study during the fall term of 1 938-39. Ann. Math. Stud., no. 3. Princeton, N. I.: Princeton U. Press, 1940. (Reprinted 1951 with corrections and three pages of notes by Godel; the seventh and eighth printings, 1966 and 1970, include additional notes and a bibliography. Russian trans. 1948, see }. Symb. Logic. 14: 142.) Consistency-proof for the generalized continuum-hypothesis. Proc. Natl. Acad. Sci. USA (communicated 14 Feb. 1939), 25:220 - 24. (Reprinted in Feigner, 1979; corrections in (1947, Ftn. 23, = Ftn. 24 in the 1964 reprint); also see Kleene 1978 and Wang 1981, Ftn. 7.) 1944 Russell's mathematical logic. In Schilpp (1944, pp. 123-531. (Re- printed, with a prefatory note by Godel, in Benacerraf and Put- nam 1964, pp. 211-32; Italian trans.: 1967, see J. Symb. Logic, 34:313; French trans.: 1969, see i. Symb. Logic, 40:281; re- printed, with Godel's 1964 prefatory note expanded, a refer- ence supplied in Ftn. 7, and Ftn. 50 omitted, in Pears 1972, pp. 1 92-226; Portuguese trans.: Lourenco 1 979, pp. 1 83 -2 1 6.) 1946 Remarks before the Princeton Bicentennial Conference on Prob- lems in Mathematics EDecember 17i, 1946. Plans for publication of the papers presented at the conference fell through, as the conferees learned only much later. When the Davis anthology

176 BIOGRAPHICAL MEMOIRS (1965) was being planned, Kleene drew the attention of the publisher to this paper of Godel and supplied a copy of the text that had been in his file since 1946, which with Godel's permis- sion (and Godel's addition of a four-line footnote) was then published as Davis (1965, 84-881. (Italian trans.: 1967, see }. Symb. Logic, 34:313; reprinted, with trifling changes in punc- tuation and phrasing, and the substitution of"It follows from the axiom of replacement" for "It can be proved" at the end, in Klibansky 1968, pp. 250 - 53; Portuguese trans.: Lourenco 1979, pp. 377-83.) 1947 What is Cantor's continuum problem? Am. Math. Mon., 54:515- 25; errata, 55:151. (Reprinted, with some revisions, a substan- tial supplement, and a postscript, by Godel, in Benacerraf and Putnam 1964, pp. 258-73; Italian trans.: 1967, see l. Symb. Logic, 34:313; Romanian trans.: Parvu 1974, pp. 317 - 38; Por- tuguese trans.: Lourenco 1979, pp. 217-44; see (1958c) and (19731.) 1949 a. An example of a new type of cosmological solutions of Einstein's field equations of gravitation. Rev. Mod. Phys., 21:447-50. b. A remark about the relationship between relativity theory and idealistic philosophy. In Schilpp (1949, pp. 555-621. (German trans., with some additions by Godel to the footnotes: Schilpp 1955, pp. 406-12.) 1950 Rotating universes in general relativity theory. In: Proc. Int. Cong. Math. (Cambridge, Mass., 1950), vol. 1, pp. 175-81. Providence, R. I.: American Mathematical Society, 1952. 1952 fA popular interview with Godel:] Inexhaustible. The New Yorker, Aug. 23, 1952, pp. 13-15. 1956 Godel expresses regret at Friedberg's intention to study medicine in: The prodigies. Time, March 19, 1956, p. 83.

.. KURT GODEL 1957 177 Kreisel (1962, pp. 140-42) states some results as having been com- municated to him by Godel in 1957. 1958 a. Uber eine bisher noch nicht benutzte Erweiterung des finiten Standpunktes. Dialectica, 12:280-87. (Reprinted in Logica, Stu- dia Paul Bernays Dedicata, Bibliotheque Scientifique no. 24, pp. 76-83. Neuchatel: Griffon, 1959. Russian trans. 1967, see I. Symb. Logic, 35: 323; English trans.: 1 980 With a bibliography of work resultingfrom this paper], J. Philos. Logic, 9:133-42. According to the review of this translation by Feferman, Math. Rev., 81i:3410-11, there was an unpublished earlier English trans., which was revised several times by Godel and "contained a number of further notes which considerably amplified and in some cases corrected both technical and philosophical points." Italian trans.: Cagnoni 1981, pp. 117-23; also see (1961) and Spector ~ 1961).) b. Kreisel (1958, pp. 321-22) attributes the substance of his re- marks 2.1 and 2.3 to Godel. c. A statement by Godel is quoted in Ulam (1958, Ftn. 5, p. 131. 1961 A postscript by Godel is on p. 27 of Spector (1961). 1963-66 c. a. Benacerraf and Putnam (1964), Davis (1965), and van Heijen- oort (1967) include various contributions by Godel to their re- prints and translations of his (1930a), (1931a), (1931b), (1934), ~ 1944), and ~ 19471. b. A letter from Godel is quoted in von Neumann (1966, pp. 55 561. A 1966 greeting by Godel is on p. (viii) of Bulloff et al. (19691. 1967 An extract from a 30 June 1967 letter from Godel is in Rautenberg (1968, p. 20~. 1973 A communication from Godel of October 1973 is quoted in Green- berg ~ 1980, p. 2501.

178 BIOGRAPHICAL MEMOIRS 1974 a. Communications from Godel are reproduced in Wang (1974, pp. 8-12, 84-88, 186-90, and 324-261. b. Godel contributed a statement to the preface to Robinson (19741. c. Reinhardt (1974, Ftn. 1, p. 189) reports on discussions with Godel. d. A 1974 memorial tribute to Robinson by Godel appears oppo- site the frontispiece of Saracino and Weispfennig (19751. 1976-77 a. Wang (1981), begins with the words, "The text of this article Lbut not the footnotes and section headings] was done together with Godel in 1976 to 1977 and was approved by him at that time." b. The text of Kleene ~ 1978) is composed of communications from Godel of May and June 1977. See Kreisel's review in the Zen- tralblatt ~ 1 979) 40 1: 1 2-1 3.