Labyrinth of Thought pp 337-364 | Cite as

# Logic and Type Theory in the Interwar Period

## Abstract

The 1920s atmosphere, among experts in foundational studies, was one of great insecurity. Most of them — intuitionists excluded — were looking for a symbolic, formal system that might provide a framework for all of mathematics. It *had* to be possible to reconstruct mathematics on a completely secure basis, to find a system maximally immune to rational doubt.^{3} But, in carrying out that project, caution was the keyword. Reminders were the by-then legendary paradoxes, which ruined the work of Frege and imperiled that of Cantor, the intuitionists’ indictment against modern mathematics, and the proliferation of divergent systems. During the interwar period there was a great level of experimentation in the area of foundations, not infrequently leading to systems that turned out to be contradictory.^{4} Even those who were convinced of the final vindication of the ‘classical’ viewpoint of Cantor and Dedekind, like Hilbert, had to look for very careful ways of proceeding if they wanted to solve satisfactorily all of the problems posed.

## Keywords

Type Theory Propositional Function Interwar Period Radical Proposal Simple Type Theory## Preview

Unable to display preview. Download preview PDF.

## References

- 1.[von Neumann 1928, 321]: “...dass es heute keine einheitliche allgemeine Mengenlehre gibt: sondern eine naive, eine intuitionistische, sowie mehrere formalistisch-axiomatische Systeme.”Google Scholar
- 2.[Church 1937, 95].Google Scholar
- 1.This viewpoint, which dominated work in logic and foundations until World War II, has been called
*foundationalism*[Shapiro 1991, 25].Google Scholar - 1.Examples are systems presented by Church in the early 30s (see [Kleene & Rosser 1935]) and Quine’s
*ML*in its original [1940] presentation (see [Rosser 1942] and [Ullian 1986; Wang 1986; Ferreirós 1997]).Google Scholar - 1.These wider aspects, including academic politics and outright political issues, have been explored by Mehrtens [1990] and van Dalen [1995].Google Scholar
- 2.He had married a disciple of Husserl; see [Weyl 1918, 35–37] [Weyl 1954].Google Scholar
- 3.[Weyl 1918, 36–37]: “Erst im Zusammenhang mit allgemeinen philosophischen Erkenntnissen, zu denen ich mich durch die Abkehr vom Konventionalismus durchrang, gelangte ich zur Klarheit darüber, dass ich hier einem scholastischen Scheinproblem nachjagte, und gewann die feste Überzeugung (in Übereinstimmung mit Poincaré, so wenig ich dessen philosophische Stellung im übrigen teile), dass die
*Vorstellung der Iteration*,*der natürlichen Zahlenreihe*,*ein letztes**Fundament des mathematischen Denkens ist —*trotz der Dedekindschen `Kettentheorie’.”Google Scholar - 4.Dieudonné in [Gillispie 1983, vol.13, 285]; as Dieudonné indicates, fortunately (or intentionally?) he dealt with theories in which he could do so with impunity.Google Scholar
- 1.More precisely, one makes the predicative levels (see below) collapse by quantifying over numbers or sets of any level whatsoever.Google Scholar
- 2.To believe his own account [1918, 35], Weyl developed his ideas before coming to know of the related ones of Frege and Russell.Google Scholar
- 1.[Weyl 1921, 149]: “Durch diese Begriffseinschränkung wird aus dem fliessenden Brei des Kontinuums sozusagen ein Haufen einzelner Punkte herausgepickt. Das Kontinuum wird in isolierte Elemente zerschlagen... Ich spreche daher von einer
*atomistischen Auffassung des Kontinuums.”*Google Scholar - 2.Also retained is a version of Cantor’s proof that the continuum is not denumerable, even though one can enumerate all possible sets of natural numbers [Weyl 1918, 25]. For further remarks on how the set-theoretical ideas of Dedekind and Cantor are affected by his proposal, see
*[op.cit.*, 16, 19, 37].Google Scholar - 1.Brouwer introduced also another notion that corresponds to a different aspect of the classical notion of set - the notion of a “species,” roughly meaning a class of mathematical entities corresponding to a given property [Brouwer 1925, 245–46]. On Brouwer’s theory of spreads and species, see [Heyting 1956; van Heijenoort 1967, 446–63; Troelstra & van Dalen 1988].Google Scholar
- 2.Years later, he wrote that only with hesitation he could acknowledge those lectures, which in their “bombastic” style reflected the mood of the excited times after World War I
*[op.cit.*, 179].Google Scholar - 3.The latter included, beyond ZFC and von Neumann’s system, the weaker ones of Russell and of Hilbert and his school
*[op.cit.*, 321–22].Google Scholar - 1.[Hilbert 1922, 159, 161–62, 174–75, 176–77].Google Scholar
- 2.[Hilbert 1922, 160] as translated in [Ewald 1996, 1119] with minor changes.Google Scholar
- 1.A more detailed presentation of the underlying ideas was given in [Hilbert 1926], and further details concerning the system in [1927].Google Scholar
- 2.See [Hilbert 1922, 176–77; 1923, 178; 1926, 383; 1927, 479].Google Scholar
- 3.See [Bernays 1935, 211] and also, e.g., [Hilbert 1929] and [Bernays 1930, 58].Google Scholar
- 1.[Gödel 1931] only contains a sketch of the proof of this second incompleteness theorem, based on the idea that some reasonings in his first incompleteness theorem could be strictly formalized. He planned to devote a second paper to the issue, but did not come to do so. See [Gödel 1986, 137–38].Google Scholar
- 2.See, e.g., [von Neumann 1947] and the `Nachtrag’ to [Bernays 1930, 60–61]. Hilbert himself did not think so [Hilbert & Bernays 1934/39]. For detailed analysis of Hilbert’s program, see [Kreisel 1978; Detlefsen 1986; Hallett 1991].Google Scholar
- 3.This historiographical point was prepared by van Heijenoort [1967] and forcefully established by Goldfarb [1979] and Moore [1988]. Moore [forthcoming] lists five main approaches around the turn of the century.Google Scholar
- 1.This is said explicitly in [Carnap 1931, 46].Google Scholar
- 2.There are indications that Hilbert abandoned that view in favor of logicism during the War (see [1918, 153; Hilbert & Ackermann 1928]), but only to return to it in the early 1920s.Google Scholar
- 3.[Skolem, 1928, 517]. This was essentially Hilbert’s viewpoint in [1904].Google Scholar
- 1.A similar tendency can be found among North-American authors such as Post, influenced by the axiomatic movement, and also, though less clearly, in Skolem (see [Dreben & van Heijenoort 1986, 44–48]).Google Scholar
- 1.See [Wiener 1914, 225]. Translated into modern notation, <
*x*,*y >*=Df_{.}{{{x},Q}, {{y}}}; this complies with type restrictions, since there is a null set for each type.Google Scholar - 2.One may conjecture that part of the difficulty during this period was that many people lacked a clear understanding of the background motivations for the different viewpoints advanced, in the present case, of the relationship between platonistic assumptions and impredicativity.Google Scholar
- 1.But in fact Ramsey lacked a clear notion of tautology; by `tautological’ he means `true for an intended interpretation’ (see, e.g., [1926, 209–10]). Strictly speaking, a proposition is a tautology iff it is true for any combination of truth-values of its constituent elementary propositions [Wittgenstein 1921, §4.46]. The doctrine of Wittgenstein and the Vienna Circle is flawed, since the notion of tautology only seems to make sense within the realm of propositional logic, as Tarski pointed out in 1934 [Tarski 1986, vol. 4, 694; 1956, 419–20].Google Scholar
- 2.[Chwistek 1921], as translated by Church [1937a, 169].Google Scholar
- 1.See [Grattan-Guinness 1979, 74], [Fraenkel, Bar-Hillel & Levy 1973, 200–05] and further references given here.Google Scholar
- 2.Nowadays, Ramsey’s `logical’ paradoxes are called set-theoretical; his terminology reflectsGoogle Scholar
- 1.Ramsey then tended to formalism with a 1928 contribution to the decision problem, establishing the theorem that bears his name, and a 1929 article for the
*Britannica;*and finally he tended to intuitionism, according to a review by Russell in*Mind***40**(1931).Google Scholar - 1.See [Carnap 1937] and [Sarkar 1992]. Of the intuitionist authors which Carnap quotes, the one who uses a system closer to language I is Weyl (§5.1). Type theory was still the preferred logical system in Carnap’s
*Introduction to Symbolic Logic*, a handbook of 1954 in the original German.Google Scholar - 2.On Church’s life and work, including a description of his system for TT and comments on the implications it had for Henkin, see [Manzano 1997] (particularly [227–29]).Google Scholar
- 3.See [Tarski 1933, 241–43] and for motivation of the system [Tarski 1931, 213–17]. Infinity was formulated by asserting the existence of a class of type 3 whose properties make necessary the existence of infinitely many individuals. Formulating the Axiom of Choice does not present any particular problem either.Google Scholar
- 1.Tarski, following his teacher Lesniewski, called instances of this axiom “pseudo-definitions.”Google Scholar
- 2.I have not formulated the axioms exactly as Gödel did, but introduced slight simplifications that involve no conceptual change. He wrote:
*(Eu)(vFH(u(v) = a))*, making explicit the type restrictions, and xlfl[x2(xt) ° Y2(xt)] D X2 = y2, indicating that we may elevate the types.Google Scholar - 3.This is actually what Tarski did. He remarks on the relation between predication and membership in [Tarski 1931, 214n].Google Scholar
- 4.See, e.g., his papers of 1924 in [Tarski 1986, vol.1, 41, 67].Google Scholar
- 1.This is the period reflected in the logical papers collected for [Tarski 1956].Google Scholar
- 2.See [Fraenkel, Bar-Hillel & Levy 1973, 188–190]. Le§niewski’s theory has an important precedent in Husserl, whose work affected Weyl in a similar way.Google Scholar
- 3.He also thought it impossible to give a formal definition of the concept of logical consequence, a view that he would correct two or three years later (see [Tarski 1956, 293–295, 413 note 2]).Google Scholar
- 4.See
*Journal of Symbolic Logic***2**(1937), 44. The question, however, is quite elementary, and there was corresponding work on ZF [Ackermann 1937].Google Scholar - 5.See, e.g., [Gödel 1931, 144–45], [Tarski 1986, vol. 1, 236 and
*passim]*, [Church 1939, 6970], or the retrospective comments in [Carnap 1963, 33].Google Scholar - 1.Another possible denomination is “finite logic”
*[op.cit.*, 21 note, 32], responding to the idea that higher-order predicative logic is “transfinite” because it requires us to overview all the derived properties and relations, not simply the initially given individuals as in restricted logic.Google Scholar - 1.In modern notation 3z
*U(x*,*y*,*z*). Weyl realized that his notation was inconvenient, but he was not interested in formalizing mathematics. Similar principles, and in particular the analogue of first-order existential quantication, were already presented in [Weyl 1910].Google Scholar - 2.Thus, to the above logical principles of construction, he added further mathematical principles — of substitution and above all of iteration (principles 7 and 8
*[op.cit.*, 24–28]). We shall not discuss them in detail; suffice it to say that they establish the possibility of recursive definitions, what Weyl calls “iteration.” For a detailed analysis see [Feferman 1988].Google Scholar - 3.For detailed analysis of these lectures, see [Moore 1997]. They were the basis for the later book [Hilbert & Ackermann 1928].Google Scholar
- 4.See [Weyl 1910] and [1918, 35–36]. Weyl moved to Zürich in 1913.Google Scholar
- 1.Löwenheim [1915] talks about “number-expressions.”Google Scholar
- 2.He proposes two ways of solving the problem. One is essentially the same as Weyl’s predicative (expanded) logic, discussed above. The other would be to axiomatize the notion of predicate, but the result would be essentially equivalent to axiomatic set theory. Thus, non-predicative higher-order logic is certainly not a good candidate for a logical basis on which to axiomatize set theory.Google Scholar
- 3.If one has goals different from providing a
*foundation*for a given theory, for instance semantic goals, it may be sound to rely on higher-order logic [Shapiro 1991]. This makes some sense of Zermelo’s work around 1930 (see [Moore 1980]).Google Scholar - 1.That a definite proposition is one for which “the fundamental relations of the domain [of the form
*a*e*b]*, by means of the axioms and the universaly valid laws of logic, determine without arbitrariness whether it holds or not” [Zermelo 1908, 201].Google Scholar - 2.Previously Skolem [1920] had offered a different proof using the Axiom of Choice and Dedekind’s theory of chains, with the stronger result that every model of the axiom system has a denumerable submodel.Google Scholar
- 3.[Skolem 1923], as translated in [van Heijenoort 1967, 293].Google Scholar
- 1.As we have seen, the result was known to him as early as 1916. He came back to the topic later, in a long paper where he also formulated explicitly a first-order version of ZF [Skolem 1929].Google Scholar
- 2.Following this trend of thought, Skolem was the first to study non-standard models of arithmetic in the 1930s.Google Scholar
- 3.Further research, particularly on unpublished material, might settle that point.Google Scholar
- 1.[Zermelo 1932, 851: “Von der Voraussetzung ausgehend, dass alle mathematischen Begriffe und Sätze durch ein
*festes endliches Zeichensystem*darstellbar sein müssten, gerät man... in die bekannte*Richardsche Antinomie’*,*wie*sie neuerdings, nachdem sie schon lange erledigt und begraben schien, im*Skolemismus*, der Lehre, dass*jede*mathematische Theorie, auch die Mengenlehre, in einem*abzählbaren Modell*realisierbar sei, ihre fröhliche Auferstehung gefunden hat.”Google Scholar - 2.A detailed discussion of Zermelo’s proposal and his discussion with Skolem can be found in [Moore 1980].Google Scholar