Kurt Gödel

First published Tue Feb 13, 2007; substantive revision Fri Dec 11, 2015

Kurt Friedrich Gödel (b. 1906, d. 1978) was one of the principal founders of the modern, metamathematical era in mathematical logic. He is widely known for his Incompleteness Theorems, which are among the handful of landmark theorems in twentieth century mathematics, but his work touched every field of mathematical logic, if it was not in most cases their original stimulus. In his philosophical work Gödel formulated and defended mathematical Platonism, the view that mathematics is a descriptive science, or alternatively the view that the concept of mathematical truth is objective. On the basis of that viewpoint he laid the foundation for the program of conceptual analysis within set theory (see below). He adhered to Hilbert's “original rationalistic conception” in mathematics (as he called it);[1] and he was prophetic in anticipating and emphasizing the importance of large cardinals in set theory before their importance became clear.

1. Biographical Sketch

Kurt Gödel was born on April 28, 1906 in what was then the Austro-Hungarian city of Brünn, and what is now Brno in the Czech Republic.

Gödel's father Rudolf August was a businessman, and his mother Marianne was a well-educated and cultured woman to whom Gödel remained close throughout his life, as witnessed by the long and wide-ranging correspondence between them. The family was well off, and Gödel's childhood was an uneventful one, with one important exception; namely, from about the age of four Gödel suffered frequent episodes of poor health, and the health problems he suffered then as well as others of various kinds were to plague him his entire life.

Health problems notwithstanding, Gödel proved to be an exemplary student at primary school and later the Gymnasium, excelling especially in mathematics, languages and religion. Upon his graduation from the Gymnasium in Brno in 1924 Gödel enrolled in the University of Vienna, attending lectures on physics, his initial field of interest, lectures on philosophy given by Heinrich Gomperz, and lectures on mathematics. Gödel took a number of physics courses during his undergraduate years, as witnessed by his university transcript; this is notable in view of Gödel's subsequent contributions to relativity in 1947. Philipp Furtwängler, cousin of the great German conductor Wilhelm Furtwängler, was one of his mathematics professors, and indeed Furtwängler's course on class field theory almost tempted Gödel to pursue his studies in that area. Gödel learned his logic from Rudolph Carnap and from Hans Hahn, eventually graduating under Hahn with a Dr.phil. in mathematics in 1929. The main theorem of his dissertation was the completeness theorem for first order logic (Gödel 1929).[2]

Gödel's university years also marked the beginning of his attendance at meetings of the Vienna Circle, a group around Moritz Schlick that quickly became known as “logical positivists,” a term coined by Feigl and Blumberg in their 1931 “Logical positivism: A new movement in European philosophy” (Feigl and Blumberg 1931). Though Gödel was not himself a logical positivist, those discussions were a crucial formative influence.

The 1930s were a prodigious decade for Gödel. After publishing his 1929 dissertation in 1930, he published his groundbreaking incompleteness theorems in 1931, on the basis of which he was granted his Habilitation in 1932 and a Privatdozentur at the University of Vienna in 1933.

Among his mathematical achievements at the decade's close is the proof of the consistency of both the Axiom of Choice and Cantor's Continuum Hypothesis with the Zermelo-Fraenkel axioms for set theory, obtained in 1935 and 1937, respectively. Gödel also published a number of significant papers on modal and intuitionistic logic and arithmetic during this period, principal among which is his “On intuitionistic arithmetic and number theory,” (Gödel 1933e), in which he showed that classical first order arithmetic is interpretable in Heyting arithmetic by a simple translation. Other publications of the 1930s include those on the decision problem for the predicate calculus, on the length of proofs, and on differential and projective geometry.

By the end of the decade both Gödel's advisor Hans Hahn and Moritz Schlick had died (the latter was assassinated by an ex-student), two events which led to a personal crisis for Gödel. Also, his appointment at the University, that of Privatdozentur, was cancelled, being replaced by the position “Dozentur neuer Ordnung,” granted to candidates only after they had passed a racial test.[3] Gödel's three trips the United States during that decade triggered an investigation. (See Sigmund 2006.) Finally, Gödel was found fit for military service by the Nazi government in 1939.

All of these events were decisive in influencing his decision to leave Austria in 1940, when he and his wife Adele emigrated to the United States. This long and difficult episode in their life is recounted by John Dawson in his biography of Gödel called “Logical Dilemmas,” (Dawson 1997) as well as by Solomon Feferman in “Gödel's Life and Work,” (Feferman 1986) to both of which the reader is referred.

Upon arrival Gödel took up an appointment as an ordinary member at the Institute for Advanced Study; he would become a permanent member of the Institute in 1946 and would be granted his professorship in 1953. (Gödel and his wife were granted American citizenship in April 1948.) He would remain at the Institute until his retirement in 1976. The Gödels never returned to Europe.

Gödel's early years at the Institute were notable for his close friendship with his daily walking partner Albert Einstein, as well as for his turn to philosophy of mathematics, a field on which Gödel began to concentrate almost exclusively from about 1943. The initial period of his subsequent lifelong involvement with philosophy was a fruitful one (in terms of publications): in 1944 he published his first philosophical paper, entitled “On Russell's Mathematical Logic” (Gödel 1944), and in 1947 he published his second, entitled “What is Cantor's Continuum Hypothesis?” (Gödel 1947). In 1949 he published his third, entitled “A Remark on the Relationship between Relativity Theory and Idealistic Philosophy.” (Gödel 1949a). The latter paper coincided with results on rotating universes in relativity he had obtained in 1949, which were first published in an article entitled: “An Example of a New Type of Cosmological Solutions of Einstein's Field Equations of Gravitation.” (Gödel 1949).

Among Gödel's other significant philosophical works of the 1940's must be counted his 1941 lecture entitled “In What Sense is Intuitionistic Logic Constructive?” (Gödel *1941) in which the notion: “computable function of finite type” is introduced. A paper based on the ideas in the lecture entitled “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes,” was published only in 1958, and the interpretation of Heyting arithmetic into the quantifier free calculus T in it became known as the “Dialectica Interpretation,” after the journal in which the article was published (Gödel 1958). (For the revision of it from 1972, see Gödel 1995.) Finally the decade saw the beginning of Gödel's intensive study of Leibniz, which, Gödel reports, occupied the period from 1943 to 1946.[4]

The 1950s saw a deepening of Gödel's involvement with philosophy: In 1951 Gödel delivered a philosophical lecture at Brown University, usually referred to as the Gibbs Lecture, entitled “Some Basic Theorems on the Foundations of Mathematics and Their Philosophical Implications” (Gödel *1951). From 1953 to 1959 Gödel worked on a submission to the Schilpp volume on Rudolf Carnap entitled “Is Mathematics a Syntax of Language?” (Gödel *1953/9-III, Gödel *1953/9-V). Gödel published neither of these two important manuscripts in his lifetime, although both would appear on two lists which were found in the Gödel Nachlass, entitled “Was ich publizieren könnte.” (In English: “What I could publish.” Both manuscripts eventually appeared in Gödel 1995.) By the decade's close Gödel developed a serious interest in phenomenology.[5]

Gödel's final years are notable for his circulation of two manuscripts: “Some considerations leading to the probable conclusion that the true power of the continuum is ℵ2,” (Gödel *1970a, *1970b) his attempt to derive the value of the continuum from the so-called scale axioms of Hausdorff, and his “Ontologischer Beweis,” (Gödel *1970) which he entrusted to Dana Scott in 1970 (though it appears to have been written earlier). Taken together, the two manuscripts are the fitting last words of someone who, in a fifty year involvement with mathematics and philosophy, pursued, or more precisely, sought the grounds for pursuing those two subjects under the single heading: “strenge Wissenschaft”—a turn of mind that had been in place from Gödel's start in 1929, when at the age of twenty-three he opened his doctoral thesis with some philosophical remarks.

Gödel died in Princeton on January 14, 1978 at the age of 71. His death certificate records the cause of death as “starvation and inanition, due to personality disorder.” His wife Adele survived him by three years.

For further biographical material, see Gödel 1987, Kleene 1987, Kreisel 1980, Taussky-Todd 1987 and Yourgrau 2005.

2. Gödel's Mathematical Work

Below is an examination of some of Gödel's main contributions in logic and set theory. This treatment of Gödel's technical work is not exhaustive, omitting discussion of Gödel's work in physics and his work on the decision problem. These will be treated in the sequel to this entry.

For a complete chronology of Gödel's work the reader is referred to that compiled by John Dawson in volume I of Gödel's Collected Works (Gödel 1986, p. 37).

2.1 The Completeness Theorem

2.1.1 Introduction

The completeness question for the first order predicate calculus was stated precisely and in print for the first time in 1928 by Hilbert and Ackermann in their text Grundzüge der theoretischen Logik (Hilbert and Ackermann 1928), a text with which Gödel would have been quite familiar.[6]

The question Hilbert and Ackermann pose is whether a certain explicitly given axiom system for the first order predicate calculus “…is complete in the sense that from it all logical formulas that are correct for each domain of individuals can be derived…” (van Heijenoort 1967, p. 48).

2.1.2 Proof of the Completeness Theorem

We give an outline of Gödel's own proof in his doctoral thesis (Gödel 1929). An essential difference with earlier efforts (discussed below and elsewhere, e.g. in Zach 1999), is that Gödel defines meticulously all the relevant basic concepts.

A “logical expression” in Gödel's terminology is a well-formed first order formula without identity. An expression is “refutable” if its negation is provable, “valid” if it is true in every interpretation and “satisfiable” if it is true in some interpretation. The Completeness Theorem is stated as follows:

Theorem 1.
Every valid logical expression is provable. Equivalently, every logical expression is either satisfiable or refutable.

Gödel's proof calculus is that of Hilbert and Ackermann's text. An expression is in normal form if all the quantifiers occur at the beginning. The degree of an expression or formula is the number of alternating blocks of quantifiers at the beginning of the formula, assumed to begin with universal quantifiers. Gödel shows that if the completeness theorem holds for formulas of degree k it must hold for formulas of degree k + 1. Thus the question of completeness reduces to formulas of degree 1. That is, it is to be shown that any normal formula (Q)φ of degree 1 is either satisfiable or refutable, where “(Q)” stands for a (non-empty) block of universal quantifiers followed by a (possibly empty) block of existential ones.

Gödel defines a book-keeping device, a well-ordering of all tuples of variables arising from a need to satisfy φ as dictated by (Q). For example, if (Q)φ is ∀x0∃x1ψ(x0, x1), we list the quantifier-free formulas ψ(xn, xn+1). (Or more precisely, finite conjunctions of these in increasing length. See below.) Then in any domain consisting of the values of the different xn, in which each ψ(xn, xn+1) is true, the sentence (Q)φ is clearly true. A crucial lemma claims the provability, for each k, of the formula (Q)φ → (Qk)φk, where the quantifier free formula φk asserts the truth of ψ for all tuples up to the kth tuple of variables arising from (Q), and (Qk)φk is the existential closure of φk. (See the example below where the definition of the φk′s is given.) This lemma is the main step missing from the various earlier attempts at the proof due to Löwenheim and Skolem, and, in the context of the completeness theorem for first order logic, renders the connection between syntax and semantics completely explicit.

Let us consider an example of how a particular formula would be found to be either satisfiable or its negation provable, following Gödel's method: Consider φ = ∀x0∃x1ψ(x0, x1), where ψ(x0, x1) is quantifier-free. We show that this is either refutable or satisfiable. We make the following definitions:

φ0 is the expression ψ(x0, x1)
φ1 is the expression ψ(x0, x1) ∧ ψ(x1, x2)
…
φn is the expression ψ(x0, x1) ∧ …∧ ψ(xn, xn+1).

The crucial lemma, referred to above, shows that from φ we can derive for each n, ∃x0…∃xn+1φn.

Case 1: For some n, φn is not satisfiable. Then, Gödel argued, using the already known completeness theorem for propositional logic,[7] that ¬φn is provable, and hence so is ∀x0,…, xn+1¬φn. Thus ¬∃x0…∃xn+1φn is provable and therefore the ¬φ is provable, i.e., φ is refutable in the Hilbert-Ackermann system. (Some partial results about propositional logic in addition to those already mentioned include the semantic completeness of the propositional calculus due to Post (1921), as well as a more general completeness theorem for the same due to Bernays in 1918; the latter appears in Bernays' unpublished Habilitationsschrift of 1918; see also Bernays 1926.)

Case 2: Each φn is satisfiable. There are only finitely many possible models with universe {x0,…, xn+1}. Gödel orders them as a tree by defining a model M to be below a model M′ if M is a submodel of M′. In this way we obtain a tree which is finitely branching but infinite. By König's Lemma there is an infinite branch B. (In the proof, Gödel explicitly constructs the branch given by König's Lemma rather than citing it by name.) The union of the models on B forms a model M with universe {x0, x1,…}. Since M satisfies each φn, the original formula φ holds in M. So φ is satisfiable and we are done.

Note that the model, in the satisfiability case of Gödel's proof, is always countable. Thus this proof of the Completeness Theorem gives also the Löweheim-Skolem Theorem (see below). Gödel extends the result to countably many formulas and to the case of first order logic with identity. He also proves the independence of the axioms.

In 1930 Gödel published the paper based on his thesis (Gödel 1930) notable also for the inclusion of the compactness theorem, which is only implicitly stated in the thesis. The theorem as stated by Gödel in Gödel 1930 is as follows: a countably infinite set of quantificational formulas is satisfiable if and only if every finite subset of those formulas is satisfiable. Gödel uses compactness to derive a generalization of the completeness theorem.

The Compactness Theorem was extended to the case of uncountable vocabularies by Maltsev in 1936 (see Mal'cev 1971), from which the Upward Löwenheim-Skolem theorem immediately follows. The Compactness Theorem would become one of the main tools in the then fledgling subject of model theory.

2.1.3 An Important Consequence of the Completeness Theorem

A theory is said to be categorical if it has only one model up to isomorphism; it is λ-categorical if it has only one model of cardinality λ, up to isomorphism. One of the main consequences of the completeness theorem is that categoricity fails for Peano arithmetic and for Zermelo-Fraenkel set theory.

In detail, regarding the first order Peano axioms (henceforth PA), the existence of non-standard models of them actually follows from completeness together with compactness. One constructs these models, which contain infinitely large integers, as follows: add a new constant symbol c to the language of arithmetic. Extend PA to a new theory PA* by adding to it the infinite collection of axioms: {c > 0, c > 1, …}, where, e.g., 3 is S(S(S(0))). PA* is finitely consistent (i.e., every finite subset of PA* is consistent) hence consistent, hence by the Completeness Theorem it has a model.

This simple fact about models of Peano arithmetic was not pointed out by Gödel in any of the publications connected with the Completeness Theorem from that time, and it seems not to have been noticed by the general logic community until much later. Skolem's definable ultrapower construction from 1933 (see Skolem 1933) gives a direct construction of a non-standard model of True Arithmetic (which extends Peano arithmetic, being the set of arithmetic sentences true in the natural numbers). But Skolem never mentions the fact that the existence of such models follows from the completeness and compactness theorems. Gödel in his review (1934c) of Skolem's paper also does not mention this fact, rather observing that the failure of categoricity for arithmetic follows from the incompleteness theorem.

As for set theory, the failure of categoricity was already taken note of by Skolem in 1923, because it follows from the Löwenheim-Skolem Theorem (which Skolem arrived at that year; see Skolem 1923, based on Löwenheim 1915 and Skolem 1920): any first order theory in a countable language that has a model has a countable model.

Skolem's observation that categoricity fails for set theory because it has countable models is now known as the Skolem paradox.[8]The observation is strongly emphasized in Skolem's paper, which is accordingly entitled ‘An Observation on the Axiomatic Foundations of Set Theory' As he wrote in the conclusion of it, he had not pointed out the relativity in set theory already in 1915 because:

… first, I have in the meantime been occupied with other problems; second, I believed that it was so clear that axiomatization in terms of sets was not a satisfactory ultimate foundation of mathematics that mathematicians would, for the most part, not be very much concerned with it. But in recent times I have seen to my surprise that so many mathematicians think that these axioms of set theory provide the ideal foundation for mathematics; therefore it seemed to me that the time had come to publish a critique. (English translation taken from van Heijenoort 1967, p. 300.)

As an aside, in the proof of the Löwenheim-Skolem theorem, specifically that part of the theorem in which one constructs a model for a satisfiable sentence, Löwenheim and Skolem's tree construction was more or less the same as appears in Gödel's thesis. In a 1967 letter to Hao Wang, Gödel takes note of the fact that his completeness proof had almost been obtained by Skolem in 1923. Though van Heijenoort and Dreben (Dreben and van Heijenoort 1986) remark that “Throughout much of the 1920s it was not semantic completeness but the decision problem for quantificational validity, a problem originating from the work of Schröder and Löwenheim, that was the dominant concern in studying quantification theory” (examples of such results would include the decision procedure for the first order monadic predicate calculus due to Behmann, (Behmann 1922)), according to Gödel, the reasons that Skolem did not obtain the complete proof are different and philosophically important, having to do with the then dominant bias against semantics and against infinitary methods:

The Completeness Theorem, mathematically, is indeed an almost trivial consequence of Skolem 1923. However, the fact is that, at that time, nobody (including Skolem himself) drew this conclusion neither from Skolem 1923 nor, as I did, from similar considerations of his own …This blindness (or prejudice, or whatever you may call it) of logicians is indeed surprising. But I think the explanation is not hard to find. It lies in the widespread lack, at that time, of the required epistemological attitude toward metamathematics and toward non-finitary reasoning. (Gödel 2003b).

The matter of Skolem's contribution to the Completeness Theorem has been extensively discussed in van Atten and Kennedy 2009, as well as in van Atten 2005.

2.2 The Incompleteness Theorems

Gödel mentioned the possibility of the unsolvability of a question about the reals already in his 1929 thesis, in arguing against the formalist principle of Hilbert's, that consistency is a criterion for existence. In fact, giving a finitary proof of the consistency of analysis was a key desideratum of what was then known as the Hilbert program, along with proving its completeness. Accordingly it was Gödel's turn to these questions, especially the first, which led him to the two incompleteness theorems. (For a discussion of the Hilbert Program the reader is referred to the standard references: Sieg 1990, 1988, 1999; Mancosu 1998, Zach 2003, Tait 1981 and Tait 2002.)

The First Incompleteness Theorem provides a counterexample to completeness by exhibiting an arithmetic statement which is neither provable nor refutable in Peano arithmetic, though true in the standard model. The Second Incompleteness Theorem shows that the consistency of arithmetic cannot be proved in arithmetic itself. Thus Gödel's theorems demonstrated the infeasibility of the Hilbert program, if it is to be characterized by those particular desiderata, consistency and completeness.

As an aside, von Neumann understood the two theorems this way, even before Gödel did. In fact von Neumann went much further in taking the view that they showed the infeasibility of classical mathematics altogether. As he wrote to Carnap in June of 1931:

Thus today I am of the opinion that 1. Gödel has shown the unrealizability of Hilbert's program. 2. There is no more reason to reject intuitionism (if one disregards the aesthetic issue, which in practice will also for me be the decisive factor). Therefore I consider the state of the foundational discussion in Königsberg to be outdated, for Gödel's fundamental discoveries have brought the question to a completely different level.[9]

And the previous fall von Neumann had written to Gödel in even stronger terms:

Thus, I think that your result has solved negatively the foundational question: there is no rigorous justification for classical mathematics. (Gödel 2003b, p. 339)

It would take Gödel himself a few years to see that those aspects of the Hilbert Program had been decisively refuted by his results (Mancosu 2004).

2.2.1 The First Incompleteness Theorem

In his Logical Journey (Wang 1996) Hao Wang published the full text of material Gödel had written (at Wang's request) about his discovery of the incompleteness theorems. This material had formed the basis of Wang's “Some Facts about Kurt Gödel,” and was read and approved by Gödel:

In the summer of 1930 I began to study the consistency problem of classical analysis. It is mysterious why Hilbert wanted to prove directly the consistency of analysis by finitary methods. I saw two distinguishable problems: to prove the consistency of number theory by finitary number theory and to prove the consistency of analysis by number theory … Since the domain of finitary number theory was not well-defined, I began by tackling the second half… I represented real numbers by predicates in number theory… and found that I had to use the concept of truth (for number theory) to verify the axioms of analysis. By an enumeration of symbols, sentences and proofs within the given system, I quickly discovered that the concept of arithmetic truth cannot be defined in arithmetic. If it were possible to define truth in the system itself, we would have something like the liar paradox, showing the system to be inconsistent… Note that this argument can be formalized to show the existence of undecidable propositions without giving any individual instances. (If there were no undecidable propositions, all (and only) true propositions would be provable within the system. But then we would have a contradiction.)… In contrast to truth, provability in a given formal system is an explicit combinatorial property of certain sentences of the system, which is formally specifiable by suitable elementary means…

We see that Gödel first tried to reduce the consistency problem for analysis to that of arithmetic. This seemed to require a truth definition for arithmetic, which in turn led to paradoxes, such as the Liar paradox (“This sentence is false”) and Berry's paradox (“The least number not defined by an expression consisting of just fourteen English words”). Gödel then noticed that such paradoxes would not necessarily arise if truth were replaced by provability. But this means that arithmetic truth and arithmetic provability are not co-extensive — whence the First Incompleteness Theorem.

This account of Gödel's discovery was told to Hao Wang very much after the fact; but in Gödel's contemporary correspondence with Bernays and Zermelo, essentially the same description of his path to the theorems is given. (See Gödel 2003a and Gödel 2003b respectively.) From those accounts we see that the undefinability of truth in arithmetic, a result credited to Tarski, was likely obtained in some form by Gödel by 1931. But he neither publicized nor published the result; the biases logicians had expressed at the time concerning the notion of truth, biases which came vehemently to the fore when Tarski announced his results on the undefinability of truth in formal systems 1935, may have served as a deterrent to Gödel's publication of that theorem.

2.2.2 The proof of the First Incompleteness Theorem

We now describe the proof of the two theorems, formulating Gödel's results in Peano arithmetic. Gödel himself used a system related to that defined in Principia Mathematica, but containing Peano arithmetic. In our presentation of the First and Second Incompleteness Theorems we refer to Peano arithmetic as P, following Gödel's notation.

Before proceeding to the details of the formal proof, we define the notion of ω-consistency used by Gödel in the First Incompleteness Theorem: P is ω-consistent if P ⊢ ¬φ(n) for all n implies P ⊬ ∃xφ(x). Naturally this implies consistency and follows from the assumption that the natural numbers satisfy the axioms of Peano arithmetic.

One of the main technical tools used in the proof is Gödel numbering, a mechanism which assigns natural numbers to terms and formulas of our formal theory P. There are different ways of doing this. The most common is based on the unique representation of natural numbers as products of powers of primes. Each symbol s of number theory is assigned a positive natural number #(s) in a fixed but arbitrary way, e.g.

#(0) = 1 #(=) = 5 #(¬) = 9
#(1) = 2 #( ( ) = 6 #(∀) = 10
#(+) = 3 #( ) ) = 7 #(vi) = 11 + i
#(×) = 4 #(∧) = 8

The natural number corresponding to a sequence w = < w0,…, wk > of symbols is

⌈w⌉ = 2#(w0) · 3#(w1) · … · pk#(wk),

where pk is the k+1st prime. It is called its Gödel number and denoted by ⌈w⌉. In this way we can assign Gödel numbers to formulas, sequences of formulas (once a method for distinguishing when one formula ends and another begins has been adopted), and most notably, proofs.

An essential point here is that when a formula is construed as a natural number, then the numeral corresponding to that natural number can occur as the argument of a formula, thus enabling the syntax to “refer” to itself, so to speak (i.e., when a numeral is substituted into a formula the Gödel number of which the numeral represents). This will eventually allow Gödel to formalize the Liar paradox (with “provability” in place of “truth”) by substituting into the formula which says, ‘the formula, whose code is x, is unprovable,’ its own natural number code (or more precisely the corresponding numeral).

Another concept required to carry out the formalization is the concept of numeralwise expressibility of number theoretic predicates. A number-theoretic formula φ(n1, …, nk) is numeralwise expressible in P if for each tuple of natural numbers (n1, …, nk):

N ⊨ φ(n1, …, nk) ⇒ P ⊢ φ(n1, …, nk)
N ⊨ ¬φ(n1, …, nk) ⇒ P ⊢ ¬φ(n1, …, nk)

where n is the formal term which denotes the natural number n. (In P, this is S(S(…S(0)…), where n is the number of iterations of the successor function applied to the constant symbol 0.) One of the principal goals is to numeralwise express the predicate

Prf(x, y): ‘the sequence with Gödel number x is a proof of the sentence with Gödel number y.’

Reaching this goal involves defining forty-five relations, each defined in terms of the preceding ones. These relations are all primitive recursive.[10] Relations needed are, among others, those which assert of a natural number that it codes a sequence, or a formula, or an axiom, or that it is the code, denoted by Sb(ru1…unZ(x1)…Z(xn)), of a formula obtained from a formula with code r by substituting for its free variable ui the xi th numeral for i = 1, …, n. The forty-fifth primitive recursive relation defined is Prf(x, y), and the forty-sixth is

Prov(y): ‘the sentence with Gödel number y is provable in P’

which without being primitive recursive, is however obtained from Prf(x, y) by existentially quantifying x. (Prov(y) satisfies only the ‘positive’ part of numeralwise expressibility, and not the negative part; but the negative part is not needed.)

In Theorem V of his paper, Gödel proves that any number theoretic predicate which is primitive recursive is numeralwise expressible in P. Thus since Prf(x, y) and substitution are primitive recursive, these are decided by P when closed terms are substituted for the free variables x and y. This is the heart of the matter as we will see. Another key point about numeralwise expressibility is that although we informally interpret, for example, Prov(Sb(ru1…unZ(x1)…Z(xn))), by: ‘the formula with Gödel number r is provable if the Gödel number for the xi th numeral is substituted in place of the i th variable,’ neither the formal statement within the theory P nor anything we prove about it appeals to such meanings. On the contrary Prov(Sb(ru1…unZ(x1)…Z(xn))), is a meaningless string of logical and arithmetical symbols. As Gödel puts it in his introduction to his theorem V, ‘The fact that can be formulated vaguely by saying that every recursive relation is definable in the system P (if the usual meaning is given to the formulas of this system) is expressed in precise language, without reference to any interpretation of the formulas of P, by the following Theorem (V) (Gödel 1986, p. 171, italics Gödel's).

Gödel in his incompleteness theorems uses a method given in what is called nowadays Gödel's Fixed Point Theorem. Although Gödel constructs a fixed point in the course of proving the incompleteness theorem, he does not state the fixed point theorem explicitly. The fixed point theorem is as follows:

Theorem 2 (Gödel's Fixed Point Theorem)
If φ(v0) is a formula of number theory, then there is a sentence ψ such that P ⊢ ψ ↔ φ(⌈ψ⌉), where ⌈ψ⌉ is the formal term corresponding to the natural number code of ⌈ψ⌉.

Proof: Let σ(x,y,z) be a formula that numeralwise expresses the number theoretic predicate ‘y is the Gödel number of the formula obtained by replacing the variable v0 in the formula whose Gödel number is x by the term z’. Let θ(v0) be the formula ∃v1(φ(v1) ∧ σ(v0, v1, v0)). Let k = ⌈θ(v0)⌉ and ψ = θ(k). Now directly by the construction P ⊢ ψ ↔ φ(⌈ψ⌉).

A sentence is refutable from a theory if its negation is provable. The First Incompleteness Theorem as Gödel stated it is as follows:

Theorem 3 (Gödel's First Incompleteness Theorem)
If P is ω-consistent, then there is a sentence which is neither provable nor refutable from P.

Proof: By judicious coding of syntax referred to above, write a formula Prf(x,y)[11] of number theory, representable in P, so that

  1. n codes a proof of φ ⇒ P ⊢ Prf(n, ⌈φ⌉).

and

  1. n does not code a proof of φ ⇒ P ⊢ ¬Prf(n, ⌈φ⌉).

Let Prov(y) denote the formula ∃x Prf(x,y)[12]. By Theorem 2 there is a sentence φ with the property

  1. P ⊢ (φ ↔ ¬Prov(⌈φ⌉)).

Thus φ says ‘I am not provable.’ We now observe, if P ⊢ φ, then by (1) there is n such that P ⊢ Prf(n, ⌈φ⌉), hence P ⊢ Prov(⌈φ⌉), hence, by (3) P ⊢ ¬φ, so P is inconsistent. Thus

  1. P ⊬ φ

Furthermore, by (4) and (2), we have P ⊢ ¬Prf(n, ⌈φ⌉) for all natural numbers n. By ω-consistency P ⊬ ∃x Prf(x, ⌈φ⌉). Thus (3) gives P ⊬ ¬φ. We have shown that if P is ω-consistent, then φ is independent of P.

On concluding the proof of the first theorem, Gödel remarks, “we can readily see that the proof just given is constructive; that is … proved in an intuitionistically unobjectionable manner…” (Gödel 1986, p. 177). This is because, as he points out, all the existential statements are based on his theorem V (giving the numeralwise expressibility of primitive recursive relations), which is intuitionistically unobjectionable.

2.2.3 The Second Incompleteness Theorem

The Second Incompleteness Theorem establishes the unprovability, in number theory, of the consistency of number theory. First we have to write down a number-theoretic formula that expresses the consistency of the axioms. This is surprisingly simple. We just let Con(P) be the sentence ¬Prov(⌈0 = 1⌉).

Theorem 4 (Gödel's Second Incompleteness Theorem) If P is consistent, then Con(P) is not provable from P.

Proof: Let φ be as in (3). The reasoning used to infer ‘if P ⊢ φ, then P ⊢ 0 ≠ 1‘ does not go beyond elementary number theory, and can therefore, albeit with a lot of effort (see below), be formalized in P. This yields: P ⊢ (Prov(⌈φ⌉) → ¬Con(P)), and thus by (3), P ⊢ (Con(P) → φ). Since P ⊬ φ, we must have P ⊬ Con(P).

The above proof (sketch) of the Second Incompleteness Theorem is deceptively simple as it avoids the formalization. A rigorous proof would have to establish the proof of ‘if P ⊢ φ, then P ⊢ 0 ≠ 1’ in P.

It is noteworthy that ω-consistency is not needed in the proof of Gödel's Second Incompleteness Theorem. Also note that neither is ¬Con(P) provable, by the consistency of P and the fact, now known as Löb's theorem, that P ⊢ Prov(⌈φ⌉) implies P ⊢ φ.

The assumption of ω-consistency in the First Incompleteness Theorem was eliminated by Rosser in 1936, and replaced by the weaker notion of consistency. Rosser's generalization involves applying the fixed point theorem to the formula R(x): ‘for all z: either z is not the Gödel number of a proof of the formula with Gödel number x or there is a proof shorter than z of the negation of (the formula with Gödel number) x’ (see Rosser 1936).

With regard to the Second Incompleteness Theorem, the argument relies in part on formalizing the proof of the First Incompleteness Theorem as we saw. This step is omitted in Gödel 1931. He planned to include the step in what would have been a second part II (see footnote 48a of Gödel 1931). But instead of writing it he turned to the continuum problem.[13] (Part II was to elaborate on other points too: the ‘true reason for incompleteness,’ and the applicability of the two theorems to other systems.) He perhaps did not feel compelled to attend to what looked like an exercise in formalization, relying instead on the informal argument to convince (in which it succeeded). However this step turned out to be somewhat non-trivial. As Kleene puts it in his introduction to Gödel 1931, of the informal presentation, “Certainly the idea of the argument for Theorem XI (consistency) was very convincing; but it turned out that the execution of the details required somewhat more work and care than had been anticipated.” (See pp. 126–141 of Gödel 1986.) Eventually a complete proof of the Second Theorem was given by Hilbert and Bernays in some seventy pages in their Hilbert and Bernays 1939. A much more compact treatment of the theorem was given by Löb in his Löb 1956, and subsequently Feferman, in his 1960 “Arithmetization of Metamathematics in a General Setting” (Feferman 1960/1961), gave a succinct and completely general treatment of both the First and Second Theorems. But see the supplementary document:

Did the Incompleteness Theorems Refute Hilbert's Program?

For more detailed discussion, see the entry on Gödel's incompleteness theorems.

2.3 Speed-up Theorems

Gödel's 1936 ‘Speed-up’ theorem, published in an abstract “On the length of proofs”, Gödel 1936 says that while some sentences of arithmetic are true but unprovable, there are other sentences which are provable, but even the shortest proof is longer than any bound given in advance as a recursive function of the sentence. More exactly:

Theorem 5.
Given any recursive function f there are provable sentences φ of arithmetic such that the shortest proof is greater than f(⌈φ⌉) in length.

The proof we will outline is sensitive to the particular concept we use for the length of a proof. Another possibility, and the one that Gödel has in mind, is the number of formulas in the proof. Buss (see below) proves the theorem in either case, so both cases are resolved.

Proof: Let f be total recursive function. By Gödel's Fixed Point theorem there is a formula φ(n) stating ‘φ(n) has no proof in PA shorter than f(n)’. This is tenable if the length is measured by number of symbols, because we only need to search through finitely many proofs shorter than f(n). Note that φ(n) is true for all n, for if φ(n) were false, then there would be a short proof of φ(n), and hence by soundness φ(n) would be true, a contradiction: φ(n) would both true and false. This can be formalized in PA and thus we get the result that for each n the sentence φ(n) is provable in PA. Since φ(n) is true for all n, it cannot have a proof in PA which is shorter than f(n).

The Speed-up Theorem is the result of contemplating and elaborating the proof of the incompleteness theorem. It applies the fixed-point technique to the concept of unprovability by a short proof, as opposed to the original idea of applying the fixed-point theorem to mere unprovability. The proof has very much the same flavor as the proof of the incompleteness theorem. Interestingly, it dates from the same year as the construction, due to Rosser, that eliminates the use of ω-consistency in the first Incompleteness Theorem; like the Speed-up Theorem of Gödel, Rosser's construction exploits the issue of short and long proofs. Gödel never submitted a proof for the Speed-up Theorem. Over the years several related proofs were published, but the first full proof of Gödel's original result was given only in 1994 by Sam Buss in his ‘On Gödel's theorems on lengths of proofs I: Number of lines and speedups for arithmetic.’ (Buss 1994). Buss also gives a second proof of the theorem which avoids self-reference, following a technique due to Statman. Gödel measures the length of proofs by the number of formulas; but there are also other possibilities, such as the number of symbols in the proof. The case of the Speed-up Theorem where the length of proof is measured by the number of symbols was proved by Mostowski in 1952 (Mostowski 1982). For proofs of similar results see Ehrenfeucht and Mycieleski 1971, and Parikh 1971. Though both measures may be equally natural candidates for measuring the length of a proof, proving the theorem for length measured by the number of symbols avoids a technical complication introduced by the other measure: there are only finitely many proofs with a given number of symbols, whereas there are infinitely many proofs with a given number of formulas.

Gödel states the Speed-up Theorem differently from the above. Let Sn be the system of logic of the n-th order, the variables of the first level being thought of as ranging over natural numbers. In this setting, variables of the second level range over sets of natural numbers and so on. Gödel's formulation is:

Theorem 6.
Let n be a natural number > 0. If f is a computable function, then there are infinitely many formulas A, provable in Sn, such that if k is the length of the shortest proof of A in Sn and l is the length of the shortest proof of A in Sn+1, then k > f(l).

Proof sketch: The idea is the following: Let φ(x) be a formula, like above, for which φ(m) does not have a short proof in Sn for any m. Suppose we have a higher type system Sn+1 in which we can prove ∀xφ(x). This proof is of constant length. Thus each φ(m) is derivable from this universal statement by one application of the logical rule ∀xφ(x) → φ(t). Thus φ(m) has in that system for all m a short proof.

What kind of stronger system can we have in which ∀xφ(x) is provable? We may consider second order logic in which we can define a predicate N(x) for the set of natural numbers and furthermore can prove of a new predicate symbol Tr(x) that it satisfies the inductive clauses of the truth definition of first order formulas of arithmetic, relativized to N. Then the stronger system can prove that provable first order sentences of arithmetic satisfy the predicate Tr . By the above argument, we can prove in the stronger system that ∀xφ(x) satisfies Tr. Then by adding a few lines we can prove each φ(n) satisfies Tr. Because of the nature of φ(n), this implies the stronger system has a (short) proof of φ(n). An alternative system is Peano's axioms PA in an extended language where we have a new predicate symbol Tr and axioms stating that the predicate Tr codes the satisfaction relation for all sentences of the vocabulary not containing Tr.

2.4 Gödel's Work in Set theory

2.4.1 The consistency of the Continuum Hypothesis and the Axiom of Choice

Gödel's proof of the consistency of the continuum hypothesis with the axioms of Zermelo-Fraenkel set theory is a tour de force and arguably the greatest achievement of his mathematical life. This is because aside from the arithmetization, virtually all of the technical machinery used in the proof had to be invented ab initio.

The Continuum Hypothesis (henceforth CH) was formulated by Georg Cantor, and was the first problem on Hilbert's list of twenty-three unsolved problems as given in his famous address to the International Mathematical Congress in Paris in 1900. The problem as stated by Hilbert is as follows: Let A be an infinite set of real numbers. Then A is either countable, or has cardinality 2ℵ0, i.e., A is in one-to-one correspondence either with the set of natural numbers or with the set of all real numbers (otherwise known as the continuum). Another way to state the continuum hypothesis is that (the first uncountably infinite cardinal) ℵ1 = 2ℵ0.

As early as 1922 Skolem speculated that the CH was independent of the axioms for set theory given by Zermelo in 1908. Nevertheless Hilbert published a (false) proof of the CH in Hilbert 1926. In 1937 Gödel proved its consistency with the axioms of ZF set theory. (Henceforth we use the standard abbreviations for Zermelo-Fraenkel set theory, ZF, and Zermelo-Fraenkel set theory with the Axiom of Choice, ZFC.) The consistency of the negation of the CH was shown by Paul Cohen in 1961 (see Cohen 1963) and hence together with Gödel's result one infers that the CH is independent of ZF (and ZFC).

Cohen invented an important new technique called forcing in the course of proving his result; this technique is at present the main method used to construct models of set theory. Forcing led to a revival of formalism among set theorists, the plurality of models being an indication of the “essential variability in set theory,” (Dehornoy 2004) and away from the notion that there is an intended model of set theory—a perspective Gödel advocated since at least 1947, if not earlier.[14] Recently there have been signs that the CH may again be coming to be regarded as a problem to be solved mathematically (with the help of course of some new evident axioms extending ZF). (See for example Woodin 2001a, 2002, 2001b, and Foreman 1998.) If any of the proposed solutions gain acceptance, this would confirm Gödel's view that the CH would eventually be decided by finding an evident extension of the ZF axioms for set theory. The program associated with this view is called “Gödel's Large Cardinal Program.”

2.4.2 Gödel's Proof of the Consistency of the Continuum Hypothesis and the Axiom of Choice with the Axioms of Zermelo-Fraenkel Set Theory

The continuum problem is solved by finding an enumeration of the reals which is indexed by the countable ordinals, a strategy which had been recognized as a promising one already by Hilbert.[15]The problem, and the intuition behind the proof, is to build a “small” model, one in which the absolute minimum number of reals is allowed, while at the same time the model is large enough to be closed under all the operations the ZF axioms assert to exist.

Gödel's is a relative consistency proof, obtained by constructing a so-called “inner model” for ZF together with the CH. An inner model is a subcollection M of the collection V of all sets (see below) which satisfies the axioms of ZF when only sets in M are considered. Gödel's inner model is called the inner model of constructible sets (see below) and is denoted by L. Whatever is true in an inner model is consistent with ZF for the same reason that any theory with a model is consistent. An artifact of the construction is that the Axiom of Choice (henceforth AC) is satisfied in Gödel's inner model and hence the consistency of the AC with ZF was established by Gödel. Later on it was shown by Sierpinski that the AC is actually a consequence of the Generalized Continuum Hypothesis or the GCH, which states that for each κ, 2κ = κ+ (see Sierpinski 1947).

Gödel published two versions of these theorems, in 1939 and in 1940, entitled “Consistency Proof for the Generalized Continuum Hypothesis,” and “The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory,” respectively. Though completely definitive, the 1939 version is lacking in a great many details, most notably the arguments showing that if L is built inside L itself, the same L results; that is to say, the so-called absoluteness arguments are missing. Also missing are the details of the proofs that the ZF axioms hold in L. Unlike the case of the Second Incompleteness Theorem, however, Gödel subsequently gave a completely detailed proof of the two theorems in the 1940 monograph. (The 1940 proof differs substantially from the first version. For details about the two proofs and the difference between them the reader is referred to Solovay 1990 and Kanamori 2006.)

We now sketch the proof of the consistency of CH and of AC with ZFC, using modern terminology. Some preliminary concepts before sketching the proof: We first define the stratified set theoretic universe, denoted V. (V is also known as the cumulative hierarchy.) It is obtained by iteration of the power set operation (℘) beginning with the null set:

V0 = ∅,
Vα+1 = ℘(Vα),
Vγ = ∪β<γ Vβ,

where α, β are any ordinals, γ is a limit ordinal and ℘(x) denotes the power set of x. Finally

V = ∪α∈Ord Vα,

where Ord denotes the class of all ordinals.

The constructible hierarchy L is likewise defined by recursion on ordinals. But whereas the full power set operation is iterated to obtain the cumulative hierarchy, the levels of the constructible hierarchy are defined strictly predicatively, that is by including at the next level only those sets which are first order definable using parameters from the previous level. More exactly, let Def(A) denote the set of all subsets of A definable in the structure < A, ∈ > by first order formulas with parameters in A. (For more on definability see the entry on model theory in this encyclopedia.)

With this notation the constructible hierarchy is defined by induction over the ordinals as follows:

L0 = ∅,
Lα+1 = Def(Lα),
Lγ = ∪α<γ Lα,
L = ∪α∈Ord Lα,

A set x is said to be constructible if x ∈ L. The axiom which states that all sets are constructible is denoted V = L and is called the Axiom of Constructibility. Note that L is a proper class and not a set; although as we will see, each Lα is a set, and the predicate “x is constructible” is actually a definable term of the language.

Our next task is to show that L is a model of ZF. A set or a class is transitive if elements of it are also subsets. By a meticulous transfinite induction, Lα can be shown to be transitive for each α; and therefore so is L itself. This fact, together with the observation that some elementary closure properties hold in L [16] is enough to show that L is a model of ZF. (Indeed, as it turns out, L is the minimal transitive model of the ZF axioms containing all the ordinals, and is therefore in this sense canonical.)

In detail, proving that the ZF axioms, apart from the comprehension axiom, are true in L, amounts to showing that, roughly speaking, any set with a property P that a ZF axiom asserts to exist, can be seen to exist in L by considering the relativization PL of the property P to L. (A property P is relativized to an inner model M by replacing every quantifier ∃xφ by ∃x(x ∈ M ∧ φ) and every quantifier ∀xφ by ∀x(x ∈ M→ φ).) As for the comprehension axiom, verifying it requires showing that the set asserted to exist is constructed at a particular successor level Lα + 1. Proving this requires an important principle of set theory which in modern terminology is called the Levy (or ZF) Reflection Principle. This principle says that any statement in the language of ZF which is true in V is already true on some level of any continuously increasing hierarchy such as L. (For the history of this principle, see Kanamori 2006.) The Levy Reflection Principle gives the level α at which the elements of the set are all constructed. Gödel did not actually have the Levy Reflection Principle but used the argument behind the proof of the principle.

Once it is established that L is a model of ZF, one can now prove that both the CH and the AC hold in L. To this end, one first shows that the definition of L is absolute for L, where absoluteness is defined as follows: given a class M, a predicate P(x) is said to be absolute for M if and only if for all x ∈ M, P(x) ↔ PM(x).

Proving that the predicate “x is constructible” is absolute requires formalizing the notion of definability, which in turn requires formalizing the notion of satisfaction. This is because the predicate “x is constructible” says of a set, that for some ordinal α, and for some formula φ with parameters in Lα, x = {y ∈ Lα | Lα ⊨ φ(y)}. This part of the proof is tedious but unproblematic.

Once the absoluteness of L is established, it follows that ZF satisfies the axiom of constructibility if it is relativized to L; that is, ZF ⊢ (V=L)L. In particular, the axiom V = L is consistent if ZF is.

We now give the idea of the proof of CH and AC in ZF + V = L. (For a detailed exposition of the proof, the reader is referred to the standard sources. See for example Devlin's chapter on constructibility in Barwise 1977; see also Kunen 1983, and Jech 2003.)

As concerns the CH, the idea behind the proof of it in L is simply the following: Gödel showed that assuming V = L, every real number occurs on some countable level of the L-hierarchy. Since every countable level is itself countable (after all, there are only countably many possible defining formulas), and there are ω1 countable levels, there must be only ω1 real numbers.

The difficulty here, if not of the whole proof altogether, lies in showing that every real is constructed already on a countable level of the L-hierarchy. To show this Gödel argued as follows: Suppose A is a real number thought of as a set of natural numbers. By a combination of the Levy Reflection principle and the Löwenheim-Skolem Theorem there is a countable submodel < M, ∈ > of < L, ∈ > satisfying a sufficiently large finite part of the ZF axioms + V = L, such that A belongs to M. By a simple procedure < M, ∈ > can be converted into a transitive model < N, ∈ >. This procedure, used by Gödel already in 1937, was explicitly isolated by Mostowski (Mostowski 1949). The resulting model is referred to as the Mostowski Collapse.

Let us pause to discuss this important technique. Suppose < M, E> is a well-founded model of the axiom of extensionality. It is a consequence of the well-foundedness of the binary predicate E on M, and of the principle of transfinite recursion, that the equation π(x) = {π(y) | y ∈ M ∧ yEx} defines a unique function on M. The range N of π is transitive, for if π(a) ∈ N and y ∈ π(a), then y = π(b) for some b ∈ M with bEa, whence π(b) ∈ N. The fact that π is an isomorphism between < M, E> and < N, ∈ > can be proved by transfinite induction on elements on M, based again on the well-foundedness of E. The well-foundedness of < M, E> is in practice often the consequence of < M, E> being a submodel of some < Vα, ε >.

We now return to the proof of the CH in L. We used the Mostowski Collapse to construct the transitive set N. As it turns out, the real number A is still an element of < N, ∈ > . By basic properties of L, < N, ∈ > must be < Lα , ∈ > for some α . Since N is countable, α is countable too. (It can be shown that |Lα| = |α| + ℵ0.) Thus A is constructible on a countable level, which was to have been shown.

As for the AC, Gödel exhibits a definable well-ordering, that is, a formula of set theory which defines, in L, a well-ordering of all of L. The formula is tedious to write down but the idea is a simple one: A set x precedes a set y in the well-ordering if and only if either x occurs in the L-hierarchy on an earlier level Lα than y, or else they occur on the same level but x is defined by a shorter formula than y, or else they are defined by the same formula but the parameters in the definition of x occur in L earlier than the parameters of y. This well-ordering of L shows that the AC holds in L.

This concludes the proof of the consistency of AC and the CH in L.

We note that Gödel proved more in his 1939 and 1940 than what was shown here, namely he proved the Generalized Continuum Hypothesis in L and hence that it's consistency with ZF.

2.4.3 Consequences of Consistency

As noted above, it was suggested already in the 1920's that the CH might be independent of ZF or ZFC. After first conjecturing that the Axiom of Constructibility might be “absolutely consistent,” meaning not falsifiable by any further extension of models of ZF + V = L,[17] in his 1947 “What is Cantor's Continuum Hypothesis?” Gödel conjectured that the CH would be shown to be independent. The main consequence of Gödel's result, then, as far as the problem of proving the independence of the CH is concerned, was that it pointed mathematicians in the direction of adding non-constructible sets to a model of set theory in order to establish the consistency of the negation of the CH. In 1961 Dana Scott proved that the failure of the Axiom of Constructibility follows from the existence of a measurable cardinal, contrary to a conjecture Gödel had made in 1940. (See Scott 1961. A cardinal κ is said to be measurable if there is a non-principal κ-complete ultrafilter in the power-set Boolean algebra of κ.) In 1963, as noted, Paul Cohen proved the consistency of the negation of the CH by adding non-constructible sets to an inner model.

What other open questions of set theory could be solved by Gödel's method? Gödel himself noted some consequences. They are related to so called projective sets of real numbers and finite sequences of real numbers. The simplest projective sets are the closed sets, also called Π10-sets. A set is Σ1n+1 if it is the projection of a Π1n-subset of the real plane. A set is Δ1n+1 if it and its complement are Σ1n+1. Gödel observed that there is both a non-Lebesgue measurable Δ12-set and an uncountable Π11-set without a perfect subset in L. (A set of reals is perfect if it is closed, non-empty, and has no isolated points. Such sets have the size of the continuum.) Gödel gave a sketch of the proof in the 1951 second printing of Gödel 1940.

It has turned out subsequently that the axiom V = L gives a virtually complete extension of ZFC. This means that, apart from sentences arising from Gödel's incompleteness theorems, essentially all set-theoretical questions can be decided by means of the axioms V = L. This is not to imply that such results are in any way trivial. Indeed, it has turned out that L is quite a complicated structure, despite its relatively simple description. As for settling open set-theoretical questions in L, the main step was the emergence of Jensen's fine structure theory of L (Jensen 1972). Recalling that the successor step Lα +1 in the definition of the constructible hierarchy adds to L all subsets of Lα definable by first order formulas φ over (Lα, ∈), fine structure theory, roughly speaking, ramifies the step from Lα to Lα+1 into smaller steps according to the complexity of the defining formula φ. Jensen established by means of his fine structure a strengthening, denoted by ◊, of CH, that he used to construct a Souslin tree in L, and a combinatorial principle □ that he used to show that the Souslin Hypothesis is consistent with CH.

2.4.4 Gödel's view of the Axiom of Constructibility

If he did not think this way from the outset, Gödel soon came to adopt the view that the Axiom of Constructibility was implausible. As he remarked at the end of his 1947 “What is Cantor's Continuum Hypothesis?”

…it is very suspicious that, as against the numerous plausible propositions which imply the negation of the continuum hypothesis, not one plausible proposition is known which would imply the continuum hypothesis. (Gödel 1990, p. 186)

Gödel was compelled to this view of L by the Leibnizian[18] idea that, rather than the universe being “small,” that is, one with the minimum number of sets, it is more natural to think of the set theoretic universe as being as large as possible.[19]This idea would be reflected in his interest in maximality principles, i.e., principles which are meant to capture the intuitive idea that the universe of set theory is maximal in the sense that nothing can be added; and in his conviction that maximality principles would eventually settle statements like the CH. As Gödel put it in a letter to Ulam in the late 1950's, about a maximality principle of von Neumann:

The great interest which this axiom has lies in the fact that it is a maximality principle, somewhat similar to Hilbert's axiom of completeness in geometry. For, roughly speaking, it says that any set which does not, in a certain well defined way, imply an inconsistency exists. Its being a maximum principle also explains the fact that this axiom implies the axiom of choice. I believe that the basic problems of set theory, such as Cantor's continuum problem, will be solved satisfactorily only with the help of stronger axioms of this kind, which in a sense are opposite or complimentary to the constructivistic interpretation of mathematics. (Ulam 1958, as quoted in Gödel 1990, p. 168; original emphasis. Note that this is different from the very similar passage Gödel 2003b, p.295.)

Twenty years earlier, in 1938, Gödel had written seemingly differently about the Axiom of Constructibility:

The proposition A (i.e., V = L) added as a new axiom seems to give a natural completion of the axioms of set theory, in so far as it determines the vague notion of an arbitrary infinite set in a definite way. (Gödel 1986, p.27)

Gödel may have meant by “natural completion” here “the correct completion,” or he may have meant to say no more than that the Axiom of Constructibility determines the notion of set in a definite way. In any case he used the term “natural” differently in a conversation with Wang on constructibility in 1972 (Wang 1996, p. 144):

Gödel talked more about the relation between axioms of infinity and the constructible universe…(he observed that) preliminary concepts such as that of constructible sets are necessary to arrive at the natural concept, such as that of set.

This is reminiscent of a remark of Hugh Woodin, that studying forcing leads to a better understanding of V — the general principle being that studying the models of a theory is not only useful to understand the theory itself, but useful to obtain a better picture of V (Woodin 1988).

For more on Gödel's program and on Gödel's program relative to the CH the reader is referred e.g., to Steel forthcoming and Feferman et al. 2000. For more on Gödel's result, its history , and its significance the reader is referred to Floyd/Kanamori 2006 and Kennedy 2006.

2.5 Gödel's Work in Intuitionistic Logic and Arithmetic

Gödel's interest in intuitionism was deep and long-lasting. Although he himself did not subscribe to that view, he made a number of important contributions to intuitionistic logic. Perhaps the importance he placed on the concept of evidence (see below) led to his close consideration of it.

We discuss Gödel's results on intuitionistic logic in their chronological order.

2.5.1 Intuitionistic Propositional Logic is not Finitely-Valued

Both many-valued logic, introduced by Łukasiewicz in the twenties (Łukasiewicz 1970) and intuitionistic logic, formalized by Heyting in 1930, fail to satisfy the law of excluded middle. It was therefore natural to ask whether intuitionistic logic can be presented as a many-valued logic, and indeed a number of logicians in the 1920's had suggested just that. In his 1932 Gödel gave a simple argument which shows that intuitionistic propositional logic cannot be thought of as a finitely-valued logic. Precisely, Gödel proved two theorems:

Theorem 7.
There is no realization with finitely many elements (truth values) for which the formulas provable in H, and only those, are satisfied (that is, yield designated values for an arbitrary assignment).

(H is intuitionistic propositional logic, after Heyting.)

Theorem 8.
Infinitely many systems lie between H and the system A of the ordinary propositional calculus, that is, there is a monotonically decreasing sequence of systems all of which include H as a subset and are included in A as subsets.

In his proof he considered for each natural number n > 0 the sentence

Fn = ∨1 ≤ i < j ≤ n pi ≡ pj.

He observed that in an n-valued logic the sentences Fm, for m > n, should be derivable. However, Gödel showed, Fn is not derivable from Heyting's axioms for any n.

Subsequently Jaśkowski (Jaśkowski 1936) showed that intuitionistic propositional logic can be given a many-valued semantics in terms of infinitely many truth-values. For further discussion of many-valued logics, see for example the entry on many-valued logic in this encyclopedia as well as van Stigt's article on intuitionistic logic in Mancosu 1998.

2.5.2 Classical Arithmetic is Interpretable in Heyting Arithmetic

We now consider Gödel 1933e, in which Gödel showed, in effect, that intuitionistic or Heyting arithmetic is only apparently weaker than classical first-order arithmetic. This is because the latter can be interpreted within the former by means of a simple translation, and thus to be convinced of the consistency of classical arithmetic, it is enough to be convinced of the consistency of Heyting arithmetic. Heyting arithmetic is defined to be the same as classical arithmetic, except that the underlying predicate logic is given by intuitionistic axioms and rules of inference (see below).

This result extends the same assertion for the propositional case. Let H denote the intuitionistic propositional logic, and A denote its classical counterpart (as above). Inductively define:

A′ ≡ ¬¬A (A atomic)
(¬A)′ ≡ ¬A′
(A → B)′ ≡ ¬(A′ ∧ ¬B′)
(A ∨ B)′ ≡ ¬(¬A′ ∧ ¬B′)
(A ∧ B)′ ≡ A′ ∧ B′

Then,

Theorem 9.
Let F be a propositional formula. Then H ⊢ F if and only if A ⊢ F′,

The theorem follows easily from the result of Glivenko (1929) that ¬F follows from H if and only if ¬F follows from A, for any propositional formula F.

Gödel's so-called double negation interpretation extends Theorem 9 to a reduction of classical first order logic to intuitionistic predicate logic. The translation in this case can be taken to map A′ to A for atomic A. Moreover, we let ∀xA(x)′ = ∀xA′(x) :

Theorem 10.
Suppose A is a first order formula. If A is provable in classical first order logic, then A′ is provable in intuitionistic first order logic.

The above result had been obtained independently by Gentzen (with Bernays), but upon hearing of Gödel's result Gentzen withdrew his paper from publication. It had also been anticipated by Kolmogorov in his 1925 “On the Principle of the Excluded Middle,” (English translation van Heijenoort 1967) but that paper was largely unknown to logicians who were outside of Kolmogorov's circle.

Bernays has written (see Bernays' entry on David Hilbert in Edwards 1967) that this result of Gödel's drew the attention of the Hilbert school to two observations: first, that intuitionistic logic goes beyond finitism, and secondly, that finitist systems may not be the only acceptable ones from the foundational point of view.

The following theorem for the case of arithmetic follows from Theorem 10:

Theorem 11.
Suppose A is a first order formula of arithmetic. If A is provable in classical Peano arithmetic, then A′ is provable in intuitionistic first order arithmetic.

For a list of the axioms and rules of intuitionistic first order logic see Gödel 1958, reprinted with detailed introductory note by A.S. Troelstra in Gödel 1990. See also Troelstra 1973, and Troelstra's “Aspects of constructive mathematics” in Barwise 1977. For a detailed proof of the above theorem the reader is referred also to the latter.

2.5.3 Intuitionistic Propositional Logic is Interpretable in S4

This result of Gödel's (Gödel 1933f), which marks the beginning of provability logic, makes exact the difference between the concept of “provability in a specified formal system” and that of “provability by any correct means.”

Gödel had already noted this difference in the introduction to his 1929 thesis. The context was the following: Gödel entertains there the possibility that his proof of the Completeness Theorem might be circular, since the law of excluded middle was used to prove it. This is because while the Completeness Theorem asserts ‘a kind of decidability,’ namely every quantificational formula is either provable or a counterexample to it can be given, ‘the principle of the excluded middle seems to express nothing other than the decidability of every problem’:

… what is affirmed (by the law of excluded middle) is the solvability not at all through specified means but only through all means that are in any way imaginable … [20]

Gödel considers intuitionistic propositional logic (henceforth IPL); he also considers a second system, classical propositional logic enriched by an operator “B”, where the intended meaning of “B” is “provable.” The axiom system now known as S4 (for a list of these axioms see for example the entry on modal logic in this encyclopedia) is added to the standard axioms for classical propositional logic together with a new rule of proof: from A, BA may be inferred. Let us call this second system G. Gödel's theorem states that IPL is interpretable in G via the following translation:

¬p ≡ ~Bp
p ⊃ q ≡ Bp → Bq
p ∨ q ≡ Bp ∨ Bq
p ∧ q ≡ Bp ∧ Bq

That is,

Theorem 12.
Let A be a formula of IPL, and let A′ be its translation. Then IPL ⊢ A implies G ⊢ A′.

Gödel conjectures that the converse implication must be true, and indeed this was shown in McKinsey and Tarski 1948.

The difference between the two notions of provability: “provable in a given formal system S” and provability by any correct means — manifests itself as a consequence of Gödel's Second Incompleteness Theorem, as follows. Let S contain Peano arithmetic, and let the operator B be interpreted as “provable in S”. If the axioms of S4 were valid for this interpretations of B, then from B(0 ≠ 1) → (0 ≠ 1), the sentence ¬B(0 ≠ 1) would be provable, contradicting the Second Incompleteness Theorem.

For further discussion of Gödel's theorem, its antecedents and its extensions, as well as its philosophical significance, the reader is referred to A.S Troelstra's introduction to 1933f.

2.5.4 Heyting Arithmetic is Interpretable into Computable Functionals of Finite Type.

Gödel's so-called Dialectica intepretation (Gödel 1958) delivers a relative consistency proof and justification for Heyting arithmetic by means of a concrete interpretation involving a system T of computable functionals of finite type. Taken together with his 1933e, which reduces classical first order arithmetic to Heyting arithmetic, a justification in these terms is also obtained for classical first order arithmetic.

Gödel's inductive definition of the notion “function of finite type” is as follows: (Gödel 1990, p. 245).

  1. The functionals of type 0 are the natural numbers.
  2. If t0,…, tk are types and we have already defined what functionals of types t0,…,tk are, then (t0,…, tk) is a type and a functional of that type assigns to every k-tuple of functionals of respective types t1,…, tk, a functional of type t0.

Gödel considers the quantifier free theory of these functionals of finite type, denoted by T. T has the following features: the language of T contains variables of each type, constants for distinguished types, and a ternary predicate =σ for equality for type σ. Equality between terms of the same type is decidable. The non-logical axioms and rules for T include the classical arithmetic axioms for 0 and successor, and the induction rule:

(F(0) ∧ (F(x0) → F(S(x0)))) → F(x0)

for quantifier-free formulas F(x0). As Gödel remarks (Gödel 1990, p. 247), the axioms for T are essentially those of primitive recursive arithmetic, except that the variables can be of any finite type.

Gödel's translation associates with every formula F(x) of the language of Peano arithmetic a formula F′(x) = ∃y∀zA(y, z, x) of the language of the theory T, where A is quantifier free and the (boldface) bound variables are finite sequences of variables thought to range over functionals of a finite type determined by the type of the variable. Intuitively, y is a concrete analogue of the abstract notion of a construction constituting the meaning of F.

Gödel's theorem is as follows:

Theorem 13.
Suppose F′ = ∃y∀zA(y, z, x). If F is provable in intuitionistic first order arithmetic, then there are computable functionals Q of finite type such that A(Q(x), z, x) is provable in T.

The proof is by induction on the structure of the proof of F in intuitionistic first order arithmetic. (For a treatment of the proof in detail, the reader is referred to Troelstra 1986.)

The importance of the theorem for foundations cannot be overstated.[21] A discussion of its generalizations, of ensuing work on functional interpretations stimulated by the theorem due to Kreisel, Tait, Howard, Feferman and others; its foundational and philosophical significance; and finally its relation particularly to the earlier, informal, proof interpretation, so-called, given by Heyting-Kolmogorov, will not be attempted here. Accordingly the reader is referred to the large literature on the subject, e.g., the abovementioned Troelstra 1986, Tait 1967, Feferman 1993 and Avigad & Feferman 1998. For interesting recent developments, e.g., in the area of relating Gödel's Dialectica interpretation and Kreisel's modified realizability, see Oliva 2006. See also van Oosten 2008.

A remark concerning the philosophical context in which Gödel presented his translation, namely finitism. The question addressed in the introduction to the paper is what abstract notions must be added to finitary mathematics in order to obtain a consistency proof for arithmetic. Equivalently: what does the finitary view presuppose, which must be given up in the light of the Second Incompleteness Theorem, if the consistency proof is to be obtained:

In any case Bernays' remark teaches us to distinguish two components of the finitary attitude; namely, first, the constructive element, which consists in our being allowed to speak of mathematical objects only insofar as we can exhibit them or actually produce them by means of a construction; second, the specifically finitistic element, which makes the further demand that the objects about which we make statements, with which the constructions are carried out and which we obtain by means of these constructions, are ‘intuitive’, that is, are in the last analysis spatiotemporal arrangements of elements whose characteristics other than their identity or nonidentity are irrelevant.… It is the second requirement that must be dropped. This fact has hitherto been taken into account by our adjoining to finitary mathematics parts of intuitionistic logic and the theory of ordinals. In what follows we shall show that, for the consistency proof of number theory, we can use, instead, the notion of computable function of finite type on the natural numbers and certain rather elementary principles of construction for such functions. (Gödel 1990, p.245).

Aside from its technical contribution, then, Gödel's 1958/72 is one of Gödel's most important philosophical works; notable for its analysis of the nature of finitary mathematics, as well as its analysis of the notions of “intuitive,” as in “intuitive knowledge,” and that of abstract versus concrete evidence.

In the next section, we turn to Gödel's philosophical views. But interested readers may wish to read a brief discussion about Gödel's Nachlass, important source of philosophical material by Gödel:

Supplement Document: Gödel's Documents

3. Gödel's Philosophical Views

Gödel's philosophical views can be broadly characterized by two points of focus, or, in modern parlance, commitments. These are: realism, namely the belief that mathematics is a descriptive science in the way that the empirical sciences are. The second commitment is to a form of Leibnizian rationalism in philosophy; and in fact Gödel's principal philosophical influences, in this regard particularly but also many others, were Leibniz, Kant and Husserl. (For further discussion of how these philosophers influenced Gödel, see van Atten and Kennedy 2003.)

The terms “Gödel's realism” and “Gödel's rationalism” must be prefaced with a disclaimer: there is no single view one could associate with each of these terms. Gödel's realism underwent a complex development over time, in both the nature of its ontological claims as well as in Gödel's level of commitment to those claims. Similarly Gödel's rationalism underwent a complex development over time, from a tentative version of it at the beginning, to what was adjudged to be a fairly strong version of it in the 1950's. Around 1959 and for some time afterward Gödel fused his rationalistic program of developing exact philosophy with the phenomenological method as developed by Husserl.

We examine these two strains of Gödel's thinking below:

3.1 Gödel's Rationalism

Gödel's rationalism has its roots in the Leibnizian thought that the world, not that which we immanently experience but that which itself gives rise to immanent experience, is perfect and beautiful, and therefore rational and ordered. Gödel's justification of this belief rests partly on an inductive generalization from the perfection and beauty of mathematics:

Rationalism is connected with Platonism because it is directed to the conceptual aspect rather than toward the (real) world. One uses inductive evidence…Mathematics has a form of perfection…We may expect that the conceptual world is perfect, and, furthermore, that objective reality is beautiful, good, and perfect. (Wang 1996, 9.4.18)

Our total reality and total experience are beautiful and meaningful—this is also a Leibnizian thought. We should judge reality by the little which we truly know of it. Since that part which conceptually we know fully turns out to be so beautiful, the real world of which we know so little should also be beautiful. (9.4.20)

Although the roots of Gödel's belief in rationalism are metaphysical in nature, his long-standing aspirations in that domain had always been practical ones. Namely, to develop exact methods in philosophy; to transform it into an exact science, or strenge Wissenschaft, to use Husserl's term.

What this means in practice is taking the strictest view possible of what constitutes the dialectical grounds for the acceptance of an assertion; put another way, a level of rigor is aspired to in philosophical arguments approaching that which is found in mathematical proofs. A formulation of the view—one which is somewhat phenomenologically colored (see below)—can be found in a document in the Gödel Nachlass. This is a fourteen item list Gödel drew up in about 1960, entitled “My Philosophical Viewpoint.” Two items on the list are relevant here:

  1. There are systematic methods for the solution of all problems (also art, etc.).
  1. There is a scientific (exact) philosophy and theology, which deals with concepts of the highest abstractness; and this is also most highly fruitful for science.

(The list was transcribed by Cheryl Dawson and was published in Wang 1996, p. 316.)

Gödel's earlier conception of rationalism refers to mathematical rigor and includes the concept of having a genuine proof, and is therefore in some sense a more radical one than that to which he would later subscribe. One can see it at work at the end of the Gibbs lecture, after a sequence of arguments in favor of realism are given:

Of course I do not claim that the foregoing considerations amount to a real proof of this view about the nature of mathematics. The most I could assert would be to have disproved the nominalistic view, which considers mathematics to consist solely in syntactical conventions and their consequences. Moreover, I have adduced some strong arguments against the more general view that mathematics is our own creation. There are, however, other alternatives to Platonism, in particular psychologism and Aristotelian realism. In order to establish Platonic realism, these theories would have to be disproved one after the other, and then it would have to be shown that they exhaust all possibilities. I am not in a position to do this now; however I would like to give some indications along these lines. (Gödel 1995, p. 321–2).

(For a penetrating analysis of this passage see Tait 2001.) Such an analysis must be based on conceptual analysis:

I am under the impression that after sufficient clarification of the concepts in question it will be possible to conduct these discussions with mathematical rigour and that the result will then be…that the Platonistic view is the only one tenable. (Gödel 1995, p. 322).

Along with the methodological component, as can be seen from the items on Gödel's list, there was also an “optimistic” component to Gödel's rationalism: once the appropriate methods have been developed, philosophical problems such as, for example, those in ethics (e.g., item 9 on the list is: “Formal rights comprise a real science.”) can be decisively solved. As for mathematical assertions, such as the Continuum Hypothesis in set theory, once conceptual analysis has been carried out in the right way, that is, once the basic concepts, such as that of “set,” have been completely clarified, the Continuum Hypothesis should be able to be decided.

Although at the time of the Gibbs lecture the analogy in Gödel's mind between philosophical and mathematical reasoning may have been a very close one, Gödel's view at other periods was that the envisaged methods will not be mathematical in nature. What was wanted was a general, informal science of conceptual analysis.

Philosophy is more general than science. Already the theory of concepts is more general than mathematics…True philosophy is precise but not specialized.

Perhaps the reason why no progress is made in mathematics (and there are so many unsolved problems), is that one confines oneself to the ext[ensional]—thence also the feeling of disappointment in the case of many theories, e.g., propositional logic and formalisation altogether. (Wang 1996, 9.3.20, 9.3.21)[22]

(See notebook Max IV, p. 198 (Gödel Nachlaß, Firestone Library, Princeton, item 030090). Transcription Cheryl Dawson; translation from the German ours; amendment ours. Gödel's dating of Max IV indicates that it is from May 1941 to April 1942. See also Gödel's letter to Bernays, Gödel 2003a, p. 283.)

An important source for understanding Gödel's advance toward a general theory of concepts are Gödel's remarks on conceptual analysis published by Hao Wang in Logical Journey. In remark 8.6.10 for example, Gödel expresses the belief that extensionality fails for concepts, contrary to what he said in his 1944 “Russell's Mathematical Logic,” a remark which he now wishes to retract:

I do not (no longer) believe that generally sameness of range is sufficient to exclude the distinctness of two concepts.

In some of Gödel's later discussions another component of conceptual analysis emerges, namely the project of finding the so-called primitive terms or concepts, and their relations. These are roughly terms or concepts which comprise a theoretical “starting point,” on the basis of their meaning being completely definite and clear. For example, the concept of “the application of a concept to another concept” is a primitive term, along with “force”. (Wang 1996, 9.1.29).

He spoke to Wang about the general project in 1972:

Phenomenology is not the only approach. Another approach is to find a list of the main categories (e.g., causation, substance, action) and their interrelations, which, however, are to be arrived at phenomenologically. The task must be done in the right manner. (Wang 1996, 5.3.7).

Gödel spoke with Sue Toledo between 1972 and 1975 about the project of finding primitive terms, as well as other aspects of phenomenology. See Toledo 2011. We discuss Gödel's involvement with phenomenology further in the supplementary document Gödel's Turn to Phenomenology.

The judgement levied upon Gödel's rationalism by contemporary philosophers was a harsh one. (See for example Gödel 1995, pp. 303–4). Nevertheless Gödel himself remained optimistic. As he commented to Wang:

It is not appropriate to say that philosophy as rigorous science is not realizable in the foreseeable future. Time is not the main factor; it can happen anytime when the right idea appears. (Wang 1996, 4.3.14).

Gödel concluded his 1944 on a similarly optimistic note.

3.2 Gödel's Realism

Gödel's realist views were formulated mostly in the context of the foundations of mathematics and set theory.

We referred above the list “What I believe,” thought to have been written in 1960 or thereabouts. Out of 14 items, only two refer to realism, remarks 10 and 12:

  1. Materialism is false.
  1. Concepts have an objective existence.

Gödel published his views on realism for the first time in his 1944. The following is one of his most quoted passages on the subject:

Classes and concepts may, however, also be conceived as real objects, namely classes as “pluralities of things,” or as structures consisting of a plurality of things and concepts as the properties and relations of things existing independently of our definitions and constructions.

It seems to me that the assumption of such objects is quite as legitimate as the assumption of physical bodies and there is quite as much reason to believe in their existence. They are in the same sense necessary to obtain a satisfactory system of mathematics as physical bodies are necessary for a satisfactory theory of our sense perceptions and in both cases it is impossible to interpret the propositions one wants to assert about these entities as propositions about the “data,” i.e., in the latter case the actually occurring sense perceptions.

Gödel's reference to the impossibility of interpreting empirical laws, or more precisely, instantiations of them—the statements “one wants to assert,”—as statements about sense perceptions, is likely an endorsement of the (then) contemporary critique of phenomenalism. The critique was based on the observation that sense data are so inextricably bound up with the conditions under which they are experienced, that no correspondence between statements about those and the statements “we want to assert” can be given (see Chisholm 1948 for example). More generally Gödel was against verificationism, namely the idea that the meaning of a statement is its mode of verification.

The analogical point in the first part of the passage was amplified by Gödel in the draft manuscript “Is Mathematics a Syntax of Language?”:

It is arbitrary to consider “This is red” an immediate datum, but not so to consider the proposition expressing modus ponens or complete induction (or perhaps some simpler propositions from which the latter follows). (Gödel 1995, p. 359)

Some writers have interpreted Gödel in this and similar passages pragmatically, attributing to him the view that because empirical statements are paradigmatic of successful reference, reference in the case of abstract concepts should be modelled causally. (See Maddy 1990.) Interpreting reference to abstract objects this way, it is argued, addresses the main difficulty associated with realism, the problem how we can come to have knowledge of abstract objects. Others have argued that Gödel had no paradigm case in mind; that for him both the empirical and the abstract case are either equally problematic, or equally unproblematic. (See Tait 1986.) The latter view is referred to as epistemological parity in van Atten and Kennedy 2003. (See also Kennedy and van Atten 2004.)

In his 1947 “What is Cantor's Continuum Problem?”, Gödel expounds the view that in the case of meaningful propositions of mathematics, there is always a fact of the matter to be decided in a yes or no fashion. This is a direct consequence of realism, for if there exists a domain of mathematical objects or concepts, then any meaningful proposition concerning them must be either true or false.[23] The Continuum Hypothesis is Gödel's example of a meaningful question. The concept “how many” leads “unambiguously” to a definite meaning of the hypothesis, and therefore it should be decidable—at least in principle. Most strikingly Gödel does not leave the matter there but goes on to offer a practical strategy for determining the value of the continuum, as well as the truth value of other axioms extending ZFC. Specifically, he offers two criteria for their decidability: the first involves conceptual analysis and is associated with Gödel's rationalistic program. (See the above section on Gödel's rationalism.) Secondly one must keep an eye on the so-called success of the axiom, as a check or indicator of which direction to look to for the solution of its truth. For example, Gödel notes in the paper that none of the consequences of the Axiom of Constructibility are very plausible. It is, then, likely false. See Maddy 2011 and Koellner 2014 for discussion of intrinsic vs extrinsic justifications for new axioms of set theory.

For further discussion of Gödel's philosophical views see the supplementary documents:

Gödel's Turn to Phenomenology

and

A Philosophical Argument About the Content of Mathematics

Bibliography

Primary Sources

Gödel's Writings

The Gödel Nachlass is located at Firestone Library of Princeton University with the exception of Gödel's preprint collection, which is housed at the library of the Institute for Advanced Study. The Nachlass itself is the property of the Institute but a microfilm copy of it may be purchased from Brill. All of Gödel's published work, together with a large number of the unpublished material from the Nachlass, together with a selection of Gödel's correspondence is published in Kurt Gödel, Collected Works, Volumes I-V.

The Collected Papers of Kurt Gödel

  • 1986, Collected Works. I: Publications 1929–1936. S. Feferman, S. Kleene, G. Moore, R. Solovay, and J. van Heijenoort (eds.), Oxford: Oxford University Press.
  • 1990, Collected Works. II: Publications 1938–1974. S. Feferman, J. Dawson, S. Kleene, G. Moore, R. Solovay, and J. van Heijenoort (eds.), Oxford: Oxford University Press.
  • 1995, Collected Works. III: Unpublished essays and lectures. S. Feferman, J. Dawson, S. Kleene, G. Moore, R. Solovay, and J. van Heijenoort (eds.), Oxford: Oxford University Press.
  • 2003a, Collected Works. IV: Correspondence A-G. S. Feferman, J. Dawson, S. Kleene, G. Moore, R. Solovay, and J. van Heijenoort (eds.), Oxford: Oxford University Press.
  • 2003b, Collected Works. V: Correspondence H-Z. S. Feferman, J. Dawson, S. Kleene, G. Moore, R. Solovay, and J. van Heijenoort (eds.), Oxford: Oxford University Press.

Selected Works of Kurt Gödel

[1929] “I”, Dissertation, University of Vienna. Reprinted in Gödel 1986, pp. 60–101.
[1930] “Die Vollständigkeit der Axiome des logischen Functionenkalküls”, Monatshefte für Mathematik und Physik, 37: 349–360. Reprinted in Gödel 1986, pp. 102–123.
[1931] “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I”, Monatshefte für Mathematik und Physik, 38: 173–198. Reprinted in Gödel 1986, pp. 144–195.
[1932] “Zum intuitionistischen Aussagenkalkül”, Anzeiger der Akademie der Wissenschaften in Wien, 69: 65–66. Reprinted in Gödel 1986, pp. 222–225.
[1933e] “Zur intuitionistischen Arithmetik und Zahlentheorie”, Ergebnisse eines mathematischen Kolloquiums, 4: 34–38. Reprinted in Gödel 1986, pp. 286–295.
[1933f] “Eine Interpretation des intuitionistischen Aussagenkalküls”, Ergebnisse eines mathematischen Kolloquiums 4, 39–40. Reprinted in Gödel 1986, pp. 300–301.
[1933i] “Zum Entscheidungsproblem des logischen Functionenkalküls”, Monatshefte für Matematik und Physik, 40: 433–443. Reprinted in Gödel 1986, pp. 306–326.
[*1933o] “The present situation in the foundations of mathematics”, manuscript. Printed in Gödel 1995, pp. 45–53.
[1934c] Review of Skolem (1933). Zentralblatt für Mathematik und ihre Grenzgebiete, 7: 193–194. Reprinted in Gödel 1986, pp. 379–380.
[1936a] “Über die Länge von Beweisen”, Ergebnisse eines mathematischen Kolloquiums, 7: 23–24. Reprinted in Gödel 1986, pp. 395–399.
[1939a] “Consistency proof for the generalized continuum hypothesis”, Proceedings of the National Academy of Sciences, U.S.A., 25: 220–224. Reprinted in Gödel 1990, pp. 28–32.
[1940] “The Consistency of the Continuum Hypothesis”, Annals of Mathematics Studies, Volume 3, Princeton: Princeton University Press. Reprinted in Gödel 1990, pp. 33–101.
[*1941] “In what sense is intuitionistic logic constructive?”, lecture manuscript. Printed in Gödel 1995, pp. 189–200.
[1944] “Russell's mathematical logic”, The Philosophy of Bertrand Russell (Library of Living Philosophers), P. Schilpp (ed.), New York: Tudor, 1951, pp. 123–153. Reprinted in Gödel 1990, pp. 119–141.
[*1946/9-B2] “Some observations about the relationship between theory of relativity and Kantian philosophy”, manuscript. Printed in Gödel 1995, pp. 230–246.
[*1946/9-C1] “Some observations about the relationship between theory of relativity and Kantian philosophy”, manuscript. Printed in Gödel 1995, pp. 247–259.
[1947] “What is Cantor's continuum problem?”, Amer. Math. Monthly, 54: 515–525. Reprinted in Gödel 1990, pp. 176–187.
[1949a] “A remark on the relationship between relativity theory and idealistic philosophy”, Albert Einstein: Philosopher-Scientist (Library of Living Philosophers), P. Schilpp (ed.), La Salle, IL: Open Court, 1949, pp. 555–562. Reprinted in Gödel 1990, pp. 202–207.
[1949] “An Example of a New Type of Cosmological Solutions of Einstein's Field Equations of Gravitation,” Reviews of Modern Physics, 21: 447–450. Reprinted in Gödel 1990, pp. 190–198.
[*1951] “Some basic theorems on the foundations of mathematics and their implications”, lecture manuscript. Printed in Gödel 1995, pp. 304–323.
[*1953/9-III] “Is mathematics a syntax of language?”, lecture manuscript. Printed in Gödel 1995, pp. 334–356.
[*1953/9-V] “Is mathematics a syntax of language?,” lecture manuscript. Printed in Gödel 1995, pp. 356–362.
[1958] “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes”, Dialectica, 12: 280–287. Reprinted in Gödel 1990, pp. 240–251.
[*1961/?] “The modern development of the foundations of mathematics in light of philosophy”, manuscript. Printed in Gödel 1995, pp. 374–387.
[1964] “What is Cantor's continuum problem?”, revised version of Gödel 1947, in Benacerraf, P. and Putnam, H. (eds.), 1983, Philosophy of mathematics: selected readings (2nd ed.), Cambridge: Cambridge University Press. Reprinted in Gödel 1990, pp. 254–270.
[*1970] “Ontological proof”, manuscript. Printed in Gödel 1995, pp. 403–404.
[*1970a] “Some considerations leading to the probable conclusion that the true power of the continuum is ℵ2”, manuscript. Printed in Gödel 1995, pp. 420–422.
[*1970b] “A proof of Cantor's continuum hypothesis from a highly plausible axioms about orders of growth”, manuscript. Printed in Gödel 1995, pp. 422–423.

Secondary Sources

  • Avigad, J. and S. Feferman, 1998, “Gödel's Functional (‘Dialectica’) Interpretation”, in Handbook of Proof Theory (Studies in Logic and the Foundations of Mathematics, Volume 137), Samuel Buss (ed.), Amsterdam: North-Holland, pp. 337-405.
  • Awodey, S. and A. W. Carus, 2010, “Gödel and Carnap”, in Kurt Gödel: Essays for his Centennial, Solomon Feferman, Charles Parsons & Stephen G. Simpson (eds.), Cambridge: Cambridge University Press.
  • Baaz, M., and C. Papadimitriou, D.Scott, H. Putnam, and C. Harper (eds.), 2011, Kurt Gödel and the Foundations of Mathematics: Horizons of Truth, Cambridge: Cambridge University Press.
  • Badesa, C., and P. Mancosu, and R. Zach, 2009, “The Development of Mathematical Logic from Russell to Tarski, 1900–1935”, in Leila Haaparanta (ed.), The History of Modern Logic. New York and Oxford: Oxford University Press:318–470..
  • Barwise, Jon (ed.), 1977, Handbook of Mathematical Logic (Studies in Logic and the Foundations of Mathematics, Volume 90), Amsterdam: North-Holland Publishing Co.
  • Behmann, Heinrich, 1922, “Beiträge, Algebra, Logik, insbesodere zum Entscheidungsproblem”, Mathematische Annalen, 86: 419–432.
  • Benacerraf, P. and H. Putnam (eds.), 1983, Philosophy of Mathematics: Selected Readings, Cambridge: Cambridge University Press, 2nd edition.
  • Bernays, Paul, 1926, “Axiomatische Untersuchung des Aussagen-Kalkuls der ‘Principia Mathematica’”, Mathematisches Zeitschrift, 25(1): 305–320.
  • Bezboruah, A., and J.C. Sheperdson, 1976, “Gödel's second incompleteness theorem for Q”, Journal of Symbolic Logic, 41 (2): 503–512.
  • Bolzano, Bernard, 1969, Wissenschaftslehre, Sections 349–391, in Bernard Bolzano — Gesamtausgabe, Reihe I/Band 13, edited and with an introduction by Jan Berg, Stuttgart-Bad Cannstatt: Frommann Holzboog.
  • Burgess, John, 2009, “”Intuitions of Three Kinds in Gödel's Views on the Continuum“”, in Interpreting GödelKennedy, J. (ed.) Cambridge: Cambridge University Press, 2014.
  • Buss, Samuel R., 1994, “On Gödel's Theorems on Lengths of Proofs. I. Number of Lines and Speedup for Arithmetics”, Journal of Symbolic Logic, 59(3): 737–756.
  • Chisholm, R., 1948, “The Problem of Empiricism”, The Journal of Philosophy, 45: 512–7.
  • Cohen, Paul, 1963, “The Independence of the Continuum Hypothesis”, Proceedings of the National Academy of Sciences of the U.S.A., 50: 1143–1148.
  • Crocco, G., 2003, “Gödel, Carnap and the Fregean Heritage”, History and Philosophy of Logic, 27: 171–191.
  • –––, 2006, “Gödel on Concepts”, Synthese, 137(1,2): 21–41.
  • Dawson, Jr., John W., 1997, Logical dilemmas: The Life and Work of Kurt Gödel, Wellesley, MA: A. K. Peters, Ltd.
  • Dehornoy, Patrick, 2004, “Progrès récents sur l'hypothèse du continu (d'après Woodin)”, Astérisque, 294: viii, 147–172.
  • Detlefsen, Michael, 1986, Hilbert's Program: An essay on mathematical instrumentalism, Dordrecht: D. Reidel.
  • –––, 2001, “What Does Gödel's Second theorem Say?”, Philosophia Mathemathica, 9(1): 37–71.
  • –––, 2014, “Completeness and the Ends of Axiomatization”, in Interpreting Gödel, Kennedy, J. (ed.) Cambridge: Cambridge University Press, 2014.
  • Dreben, B. and J. van Heijenoort, 1986, “Introductory Note to 1929, 1930 and 1930a”, in Gödel 1986, pp. 44–59.
  • Edwards, Paul (ed.), 1967, The Encyclopedia of Philosophy, New York: MacMillan.
  • Ehrenfeucht, A. and J. Mycielski, 1971, “Abbreviating Proofs by Adding New Axioms”, Bulletin of the American Mathematical Society, 77: 366–367.
  • Feferman, Solomon, 1960/1961, “Arithmetization of Metamathematics in a General Setting”, Fundamenta Mathematicae, 49: 35–92.
  • –––, 1993, “Gödel's Dialectica Interpretation and Its Two-way Stretch”, in Computational Logic and Proof Theory (Lecture Notes in Computer Science, Volume 713), G. Gottlob, A. Leitsch, and D. Mundici (eds.), Berlin: Springer, pp. 23–40.
  • –––, 1986, “Gödel's Life and Work”, in Gödel 1986, pp. 1–34.
  • –––, 1988, “Hilbert's Program Relativized: Proof-Theoretical and Foundational Reductions”, Journal of Symbolic Logic, 53: 364–384.
  • –––, 1996, “Proof Theory”, in The Encyclopedia of Philosophy Supplement, D. Borchrt (ed.), New York: MacMillan, pp. 466–469.
  • Feferman, S., and H. Friedman, P. Maddy, and J. Steel, 2000, “Does Mathematics Need New Axioms?”, Bulletin of Symbolic Logic, 6(4): 401–446.
  • Feferman, S., C. Parsons, and S. Simpson (eds.), 2010, Kurt Gödel: Essays for his Centennial (Lecture Notes in Logic, 33), Cambridge: Cambridge University Press.
  • Feigl, H. and A. Blumberg, 1931, “Logical Positivism. A New Movement in European Philosophy”, Journal of Philosophy, 28: 281–296.
  • Floyd, J. and A. Kanamori, 2006, “How Gödel Transformed Set Theory”, Notices of the American Mathematical Society, 53(4): 419–427.
  • Folina, Janet, 2014, “Gödel on How to Have your Mathematics and Know it Too”, in Interpreting Gödel, Kennedy, J. (ed.) Cambridge: Cambridge University Press, 2014.
  • Føllesdal, Dagfinn, 1995, “Gödel and Husserl”, in From Dedekind to Gödel (Synthese Library, Volume 251), J. Hintikka (ed.), Dordrecht, Boston: Kluwer, pp. 427–446.
  • Foreman, Matthew, 1998, “Generic Large Cardinals: New Axioms for Mathematics?”, in Documenta Mathematica, Extra Volume, Proceedings of the International Congress of Mathematicians, II, pp. 11–21 [available online (in compressed Postscript)].
  • Franks, Curtis, 2009, “The Autonomy of Mathematical Knowledge: Hilbert's Program Revisited”, Cambridge: Cambridge University Press.
  • –––, 2011, “Stanley Tennenbaum's Socrates”, in Set Theory, Arithmetic and Foundations of Mathematics: Theorems, Philosophies, Kennedy, J. and Kossak, R., (eds.), Lecture Notes in Logic, 36, Cambridge: Cambridge University Press, 2011.
  • –––, 2014, “Logical Completeness, Form and Content: An Archaeology”, in Interpreting Gödel, Kennedy, J. (ed.) Cambridge: Cambridge University Press, 2014.
  • Gaifman, H., 2000, “What Godel's Incompleteness Result Does and Does Not Show”, Journal of Philosophy, 97 (8): 462–471.
  • Garson, James, 2003, “Modal Logic”, in The Stanford Encyclopedia of Philosophy, Fall 2003 Edition, Edward N. Zalta (ed.), URL = <https://plato.stanford.edu/archives/fall2003/entries/logic-modal/>.
  • Glivenko, V., 1929, “Sur quelques points de la logique de m. Brouwer.”, Académie Royale de Belgique, Bulletin de la Classe des Sciences, 15: 183–188.
  • Gottwald, Siegfried, 2004, “Many-valued Logic”, in The Stanford Encyclopedia of Philosophy, Winter 2004 Edition, Edward N. Zalta (ed.), URL = <https://plato.stanford.edu/archives/win2004/entries/logic-manyvalued/>.
  • Gödel, Rudolf, 1983, “History of the Gödel Family”, Susan Simonsin (trans.), in Weingartner and Schmetterer 1987, pp. 11–27.
  • Hauser, Kai, 2006, “Gödel's Program Revisited, Part 1: the Turn to Phenomenology”, Bulletin of Symbolic Logic, 12 (4): 529–590.
  • Heyting, Arendt, 1930, “Die formalen Regeln der intuitionistischen Logik”, Sitzungsberichte der Preussischen Akademie der Wissenschaften, physikalisch-mathematische Klasse, II, pp. 42–56.
  • Hilbert, David, 1926, “Über das Unendliche”, Mathematische Annalen, 95: 161–190.
  • Hilbert, D. and W. Ackermann, 1928, Grundzüge der theoretischen Logik, Berlin: Springer-Verlag.
  • Hilbert, D. and P. Bernays, 1934, Grundlagen der Mathematik, Volume 1, Berlin: Springer-Verlag.
  • –––, 1939, Grundlagen der Mathematik, Volume II, Berlin: Springer-Verlag.
  • Hodges, Wilfrid, 2005, “Model Theory”, in The Stanford Encyclopedia of Philosophy, Fall 2005 Edition, Edward N. Zalta (ed.), URL = <https://plato.stanford.edu/archives/fall2005/entries/model-theory/>.
  • Husserl, Edmund, 1911, “Philosophie als strenge Wissenschaft”, Logos, 1: 289–341.
  • Jaśkowski, Stanisław, 1936, “Investigations into the System of Intuitionist Logic”, Studia Logica, 34(2) (1975): 117–120. (Translated by S. McCall from the French “Rechereches sur le système de la logique intuitioniste” in Actes du Congrés International de Philosophie Scientifique, Volume VI, Hermann, Paris, 1936, pp. 58–61.)
  • Jech, Thomas, 2003, Set theory, (Springer Monographs in Mathematics), Berlin: Springer-Verlag. 3rd millennium edition, revised and expanded.
  • Jensen, R. Björn, 1972, “The Fine Structure of the Constructible Hierarchy” (with a section by Jack Silver), Annals of Mathematical Logic, 4: 229–308; Erratum, 4 (1972): 443.
  • Kanamori, Aki, 1996, “The Mathematical Development of Set theory from Cantor to Cohen.” Bulletin of Symbolic Logic, 2(1): 1–71.
  • –––, 2006, “Levy and Set Theory”, Annals of Pure and Applied Logic, 140(3): 233–252.
  • Kennedy, Juliette, 2006, “Incompleteness — A Book Review,” Notices of the American Mathematical Societ, 53(4): 448–455.
  • –––, 2011, “Gödel's Thesis: An Appreciation” in Kurt Gödel and the Foundations of Mathematics: Horizons of Truth, M. Baaz, C. Papadimitriou, D. Scott, H. Putnam, and C. Harper (eds.), Cambridge: Cambridge University Press 95–110.
  • –––, 2013, “On Formalism Freeness: Implementing Gödel's 1946 Princeton Bicentennial Lecture”, Bulletin of Symbolic Logic, 19(3): 351–393.
  • –––, 2014, “Gödel's 1946 Princeton Bicentennial Lecture: An Appreciation”, in Interpreting Gödel: Critical Essays, Cambridge: Cambridge University Press.
  • Kennedy, Juliette (ed.), 2014, Interpreting Gödel: Critical Essays, Cambridge: Cambridge University Press.
  • Kennedy, J. and van Atten, M., 2003, “On the Philosophical Development of Kurt Gödel”, Bulletin of Symbolic Logic, 9(4): 425–476. Reprinted in Kurt Gödel: Essays for his Centennial, Solomon Feferman, Charles Parsons and Stephen G. Simpson (eds.), Cambridge: Cambridge University Press.
  • –––, 2004, “Gödel's Modernism: On Set-theoretic Incompleteness”, Graduate Faculty Philosophy Journal, 25(2): 289–349. (See the Erratum in Graduate Faculty Philosophy Journal, 26(1) (2005), page facing contents.)
  • –––, 2009, “Gödel's Modernism: On Set-theoretic Incompleteness, Revisited”, in Logicism, Intuitionism and Formalism: What has become of them?, S. Linström, E. Palmgren, K. Segerberg, and V. Stoltenberg-Hansen (eds.), Berlin: Springer: 303–356.
  • –––, 2009, “Gödel's Logic”, in D. Gabbay and J. Woods (eds.), The Handbook of the History of Logic: Logic from Russell to Gödel, Volume 5, Amsterdam: Elsevier: 449–509.
  • Kleene, S. C., 1987, “Gödel's Impression on Students of Logic in the 1930s”, in Weingartner and Schmetterer 1987, pp. 49–64.
  • Koellner, Peter, 2014, “Large Cardinals and Determinacy”, The Stanford Encyclopedia of Philosophy (Spring Edition), Edward N. Zalta (ed.), URL = <https://plato.stanford.edu/archives/spr2014/entries/large-cardinals-determinacy/>.
  • Kreisel, Georg, 1980, “Kurt Gödel, 28 April 1906 – 14 January 1978”, Biographical Memoirs of Fellows of the Royal Society, 26: 148–224. Corrigenda, 27 (1981): 697; further corrigenda, 28 (1982): 697.
  • –––, 1988, “Review of Kurt Gödel: Collected works, Volume I”, Notre Dame Journal of Formal Logic, 29(1): 160–181.
  • –––, 1990, “Review of Kurt Gödel: Collected Works, Volume II”, Notre Dame Journal of Formal Logic, 31(4): 602–641.
  • –––, 1998, “Second Thoughts Around Some of Gödel's Writings: A Non-academic Option”, Synthese, 114(1): 99–160.
  • Kripke, Saul, 2009, “The collapse of the Hilbert program: why a system cannot prove its own 1-consistency”, Bulletin of Symbolic Logic, 15 (2): 229–231.
  • Kunen, Kenneth, 1983, Set Theory: An Introduction to Independence Proofs, (Studies in Logic and the Foundations of Mathematics, Volume 102), Amsterdam: North-Holland Publishing Co. Reprint of the 1980 original.
  • Löb, M. H., 1956, “Formal Systems of Constructive Mathematics”, Journal of Symbolic Logic, 21: 63–75.
  • Löwenheim, L., 1915, “Über Möglichkeiten im Relativkalkül”, Mathematische Annalen, 76(4): 447–470.
  • Łukasiewicz, Jan, 1970, Selected works, (Studies in Logic and the Foundations of Mathematics), L. Borkowski (ed.), Amsterdam: North-Holland Publishing Co.
  • Maddy, Penelope, 1990, Realism in Mathematics, New York: Clarendon Press.
  • Maddy, Penelope, 2011, Defending the Axioms, Oxford: Oxford University Press.
  • Mal'cev, Anatoli Ivanovic, 1971, The Metamathematics of Algebraic Systems. Collected Papers: 1936–1967 (Studies in Logic and the Foundations of Mathematics, Volume 66), translated, edited, and provided with supplementary notes by Benjamin Franklin Wells, III, Amsterdam: North-Holland Publishing Co.
  • Mancosu, Paolo, 1998, From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s, Oxford: Oxford University Press.
  • –––, 2004, “Review of Kurt Gödel, Collected Works, Volumes IV and V”, Notre Dame Journal of Formal Logic, 45: 109–125.
  • Martin, D.A., 2005, “Gödel's Conceptual Realism”, Bulletin of Symbolic Logic, 11: 207–224.
  • McKinsey, J. C. C. and A. Tarski, 1948, “Some Theorems About the Sentential Calculi of Lewis and Heyting”, Journal of Symbolic Logic, 13: 1–15.
  • Mostowski, Andrzej, 1949, “An Undecidable Arithmetical Statement”, Fundamenta Mathematicae, 36: 143–164.
  • –––, 1982, Sentences Undecidable in Formalized Arithmetic: An Exposition of the Theory of Kurt Gödel, Westport, CT: Greenwood Press. Reprint of the 1952 original.
  • Oliva, Paulo, 2006, “Unifying Functional Interpretations”, Notre Dame Journal of Formal Logic, 47(2): 263–290.
  • Parikh, Rohit, 1971, “Existence and Feasibility in Arithmetic”, Journal of Symbolic Logic, 36: 494–508.
  • Parsons, Charles, 1995a, “Platonism and Mathematical Intuition in Kurt Gödel's Thought”, Bulletin of Symbolic Logic, 1(1): 44–74.
  • –––, 1995b, “Quine and Gödel on Analyticity”, in On Quine: New Essays, Cambridge: Cambridge University Press, pp. 297–313.
  • –––, 2000, “Reason and Intuition”, Synthese, 125(3): 299–315.
  • –––, 2002, “Realism and the Debate on Impredicativity, 1917–1944”, in Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, (Lecture Notes in Logic, Volume 15), W. Sieg, R. Sommer, and C. Talcott (eds.), Urbana, IL: Association of Symbolic Logic, pp. 372–389.
  • –––, 2010, “Gödel and Philosophical Idealism”Philosophia Mathematica, 18 (2): 166–192.
  • –––, 2014, “Analyticity for Realists”, in Interpreting Gödel, Kennedy, J. (ed.) Cambridge: Cambridge University Press, 2014.
  • Poonen, Bjorn, 2014, “Undecidable Problems: A Sampler”, in Interpreting Gödel: Critical Essays, Cambridge: Cambridge University Press.
  • Post, Emil L., 1921, “Introduction to a General Theory of Elementary Propositions”, American Journal of Mathematics, 43(3): 163–185.
  • Pudlák, Pavel, 1996, “On the lengths of proofs of consistency: a survey of results”, Annals of the Kurt Gödel Society, 2: 65-86.
  • Raatikainen, P., 2005, “On the Philosophical Relevance of Gödel's Incompleteness Theorems”, Revue Internationale de Philosophie, 59 (4): 513–534.
  • Rogers, Jr., Hartley, 1967, Theory of Recursive Functions and Effective Computability, New York: McGraw-Hill Book Co.
  • Rosser, J.B., 1936, “Extensions of Some Theorems of Gödel and Church”, Journal of Symbolic Logic, 1(3): 87–91.
  • Scott, Dana, 1961, “Measurable Cardinals and Constructible Sets”, Bulleint de l'Academie Polonaise des Sciences (Série des Science, Mathématiques, Astronomiques et Physiques), 9: 521–524.
  • Shelah, Saharon, 2014, “Reflecting on Logical Dreams”, in Interpreting Gödel: Critical Essays, Cambridge: Cambridge University Press.
  • Sieg, Wilfried, 1988, “Hilbert's Program Sixty Years Later”, Journal of Symbolic Logic, 53(2): 338–348.
  • –––, 1990, “Relative Consistency and Accessible Domains”, Synthese, 84(2): 259–297.
  • –––, 1999, “Hilbert's Programs: 1917–1922”, Bulletin of Symbolic Logic, 5(1): 1–44.
  • –––, 2006, “Gödel on Computability”, Philosophia Mathematica, 14: 189–207.
  • Sierpinski, Wacław, 1947, “L'hypothèse généralisée du continu et l'axiome du choix”, Fundamenta Mathematicae, 34: 1–5.
  • Sigmund, Karl, 2006, “Pictures at an Exhibition”, Notices of the American Mathematical Society, 53(4): 428–432.
  • Skolem, Thoralf, 1920, “Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen”, Skrifter utgit av Videnskappsselskapet i Kristiania, I. Matematisk-naturvidenskabelig klasse, Number 4, pp. 1–36. Reprinted in Skolem 1970, pp. 103–136.
  • –––, 1923, “Einige Bemerkungen zur axiomatischen Begründung der Mengenlehre”, Matematikerkongressen i Helsingfors den 4–7 Juli 1922, Den femte skandinaviska matematikerkongressen, Redogörelse, Helsinki, pp. 217–232. Reprinted in Skolem 1970, pp. 137–152.
  • –––, 1933, “Über die Unmöglichkeit einer vollständigen Charakterisierung der Zahlenreihe mittels eines endlichen Axiomensystems”, Norsk Matematisk forenings skrifter, 10: 73–82.
  • –––, 1970, Selected Works in Logic, Jens Erik Fenstad (ed.), Oslo: Universitetsforlaget.
  • Smith, David Woodruff, 2005, “Phenomenology”, in The Stanford Encyclopedia of Philosophy (Winter Edition), Edward N. Zalta (ed.), URL = <https://plato.stanford.edu/archives/win2005/entries/phenomenology/>.
  • Solovay, Robert, 1990, “Introductory Note to 1938, 1939, 1939a, 1940”, in Gödel 1990, pp. 1–25.
  • Steel, John, 2000, “Mathematics Needs New Axioms”, Bulletin of Symbolic Logic, 6(4): 422–433.
  • Steel, John, 2014, “Gödel's Program”, in Interpreting Gödel, Kennedy, J. (ed.) Cambridge: Cambridge University Press, 2014.
  • Tait, William, 1967, “Intensional Interpretations of Functionals of Finite Type I,” Journal of Symbolic Logic, 32(2): 198–212.
  • –––, 1981, “Finitism”, Journal of Philosophy, 78: 524–556. Reprinted in Tait 2005, pp. 21–42.
  • –––, 1986, “Truth and Proof: The Platonism of Mathematics”, Synthese, 69(3): 341–370. Reprinted in Tait 2005, pp. 61–88.
  • –––, 2001, “Gödel's Unpublished Papers on Foundations of Mathematics”, Philosophia Mathematica, 9(1): 87–126. Reprinted in Tait 2005, pp. 276–313.
  • –––, 2002, “Remarks on Finitism”, in Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman (Lecture Notes in Logic, Volume 15), W. Sieg, R. Sommer, and C. Talcott (eds.), Urbana, IL: Association of Symbolic Logic, pp. 410–419. Reprinted in Tait 2005, pp. 43–53.
  • –––, 2005, The Provenance of Pure Reason: Essays in the Philosophy of Mathematics and its History (Logic and Computation in Philosophy), New York: Oxford University Press.
  • –––, 2006, “Gödel's correspondence on proof theory and constructive mathematics”Philosophia Mathematica, 14 (1): 76–111.
  • –––, 2006, “Gödel's interpretation of intuitionism”,Philosophia Mathematica, 14 (2): 208–228.
  • Taussky-Todd, Olga, 1983, “Remembrances of Kurt Gödel”, in Weingartner and Schmetterer 1987, pp. 29–41.
  • Tieszen, Richard, 1992, “Kurt Gödel and Phenomenology”, Philosophy of Science, 59(2): 176–194.
  • –––, 2002, “Gödel and the Intuition of Concepts”, Synthese, 133 (3): 363–391.
  • –––, 2005, Phenomenology, Logic and the Philosophy of Mathematics, Cambridge: Cambridge University Press.
  • –––, 2011, After Gödel: Platonism and Rationalism in Mathematics and Logic, Oxford: Oxford University Press.
  • Toledo, Sue, 2011, “Sue Toledo's Notes of her Conversations with Kurt Gödel in 1972-5”, in Set Theory, Arithmetic and Foundations of Mathematics: Theorems, Philosophies (Lecture Notes in Logic, 36), Kennedy, J. and Kossak, R., (eds.), Cambridge: Cambridge University Press, forthcoming.
  • Tragesser, Robert, 1977, Phenomenology and Logic, Ithaca: Cornell University Press.
  • –––, 1984, Husserl and Realism in Logic and Mathematics, (Series: Modern European Philosophy), Cambridge: Cambridge University Press.
  • –––, 1989, “Sense Perceptual Intuition, Mathematical Existence, and Logical Imagination”, Philosphia Mathematica, 4(2): 154–194.
  • Troelstra, A. S., 1986, “Note to 1958 and 1972”, in Gödel 1990, pp. 217–241.
  • Troelstra, A. S. (ed.), 1973, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, (Lecture Notes in Mathematics, Volume 344), Berlin: Springer-Verlag.
  • Turing, A. M., 1937, “On Computable Numbers, with an Application to the Entscheidungsproblem”, Proceedings of the London Mathematical Society (Series 2), 42: 230–265.
  • van Atten, Mark, 2005, “On Gödel's Awareness of Skolem's Helsinki Lecture”, History and Philosophy of Logic, 26(4): 321–326.
  • –––, 2006, “Two Draft Letters from Gödel on Self-knowledge of Reason”, Philosophia Mathematica, 14(2): 255–261.
  • –––, 2015, “Essays on Gödel's Reception of Leibniz, Husserl and Brouwer”, Springer.
  • van Heijenoort, J. (ed.), 1967, From Frege to Gödel: A sourcebook in mathematical logic, 1879–1931, Cambridge, MA: Harvard University Press.
  • van Oosten, Jaap, 2008, Realizability: An Introduction to its Categorical Side (Studies in Logic and Foundations of Mathematics: Volume 152), Amsterdam: Elsevier.
  • von Neumann, John, 2005, John von Neumann: Selected Letters (History of Mathematics, Volume 27), foreword by P. Lax, introduction by Marina von Neumann Whitman, preface and introductory comments by Miklós Rédei (ed.), Providence, RI: American Mathematical Society.
  • Väänänen, Jouko, 2014, “Multiverse Set Theory and Absolutely Undecidable Propositions”, in Interpreting Gödel, J. Kennedy (ed.), Cambridge: Cambridge University Press, 2014.
  • Wang, Hao, 1957, “The Axiomatization of Arithmetic”, Journal of Symbolic Logic, 22: 145–158.
  • –––, 1973, From Mathematics to Philosophy, London: Routledge.
  • –––, 1981, “Some Facts about Kurt Gödel”, Journal of Symbolic Logic, 46(3): 653–659.
  • –––, 1987, Reflections on Kurt Gödel, Cambridge, MA: MIT Press.
  • –––, 1993, Popular Lectures on Mathematical Logic, New York: Dover Publications Inc., 2nd edition.
  • –––, 1996, A Logical Lourney: From Gödel to Philosophy (Representation and Mind), Cambridge, MA: MIT Press.
  • Weingartner, P., and L. Schmetterer (eds.), 1987, Gödel Remembered: Salzburg 10–12 July 1983, (History of Logic, Number 4), Naples: Bibliopolis.
  • Wilkie, Alex, and J.B. Paris, 1987, “On the scheme of induction for bounded arithmetic formulas”, 35: 261–302.
  • Woodin, W. Hugh, 1988, “Supercompact Cardinals, Sets of Reals, and Weakly Homogeneous Trees”, Proceedings of the National Academy of Sciences of the U.S.A., 85(18): 6587–6591.
  • –––, 2001a, “The Continuum Hypothesis. I”, Notices of the American Mathematical Society, 48(6): 567–576.
  • –––, 2001b, “The Continuum Hypothesis. II”, Notices of the American Mathematical Society, 48(7): 681–690.
  • –––, 2002, “Correction: ‘The Continuum Hypothesis. II’”, Notices of the American Mathematical Society, 49(1): 46.
  • Yourgrau, Palle, 2005, A World Without Time. The Forgotten Legacy of Gödel and Einstein, New York: Basic Books.
  • Zach, Richard, 1999, “Completeness Before Post: Bernays, Hilbert, and the Development of Propositional Logic”, Bulletin of Symbolic Logic, 5(3): 331–366.
  • –––, 2003, “Hilbert's Program”, in The Stanford Encyclopedia of Philosophy (Fall Edition), Edward N. Zalta (ed.), URL = <https://plato.stanford.edu/archives/fall2003/entries/hilbert-program/>.

Other Internet Resources

Acknowledgments

This entry was very much improved by discussion and correspondence with the following: Aki Kanamori, who made helpful corrections and comments to section 2.4; Jouko Väänänen, whose expertise in all areas of mathematical logic the author benefited from in a great many invaluable discussions regarding the material in section 2; my sub-editor Richard Zach, whose many important and helpful suggestions led to a vast improvement of this entry, and an anonymous referee for helpful comments and corrections. The author is grateful to the NWO for their support during the last period of the writing of this entry, to the Institute for Advanced Study for their hospitality during the writing of this entry, and to Marcia Tucker of the IAS and the Rare Books and Special Collections department of Firestone Library for all of their assistance over the years .

Copyright © 2015 by
Juliette Kennedy <juliette.kennedy@helsinki.fi>

This is a file in the archives of the Stanford Encyclopedia of Philosophy.
Please note that some links may no longer be functional.
[an error occurred while processing the directive]