In this paper, we sketch the development of two important themes of modern set theory, both of which can be regarded as growing out of work of Kurt Gödel. We begin with a review of some basic concepts and conventions of set theory.

§0. The ordinal numbers were Georg Cantor's deepest contribution to mathematics. After the natural numbers 0, 1, …, n, … comes the first infinite ordinal number ω, followed by ω + 1, ω + 2, …, ω + ω, … and so forth. ω is the first limit ordinal as it is neither 0 nor a successor ordinal. We follow the von Neumann convention, according to which each ordinal number α is identified with the set {ν ∣ ν α} of its predecessors. The ∈ relation on ordinals thus coincides with <. We have 0 = ∅ and α + 1 = α ∪ {α}. According to the usual set-theoretic conventions, ω is identified with the first infinite cardinal ℵ0, similarly for the first uncountable ordinal number ω1 and the first uncountable cardinal number ℵ1, etc. We thus arrive at the following picture:

The von Neumann hierarchy divides the class V of all sets into a hierarchy of sets Vα indexed by the ordinal numbers. The recursive definition reads: (where } is the power set of x);

Vλ = ∪v<λVv for limit ordinals λ. We can represent this hierarchy by the following picture.

§1. Introduction. Among the most remarkable discoveries in set theory in the last quarter century is the rich structure of the arithmetic of singular cardinals, and its deep relationship to large cardinals. The problem of finding a complete set of rules describing the behavior of the continuum function 2ℵα for singular ℵα's, known as the Singular Cardinals Problem, has been attacked by many different techniques, involving forcing, large cardinals, inner models, and various combinatorial methods. The work on the singular cardinals problem has led to many often surprising results, culminating in a beautiful theory of Saharon Shelah called the pcf theory (“pcf” stands for “possible cofinalities”). The most striking result to date states that if 2ℵn < ℵω for every n = 0, 1, 2, …, then 2ℵω < ℵω4.

In this paper we present a brief history of the singular cardinals problem, the present knowledge, and an introduction into Shelah's pcf theory. In Sections 2, 3 and 4 we introduce the reader to cardinal arithmetic and to the singular cardinals problems. Sections 5, 6, 7 and 8 describe the main results and methods of the last 25 years and explain the role of large cardinals in the singular cardinals problem. In Section 9 we present an outline of the pcf theory.

§2. The arithmetic of cardinal numbers. Cardinal numbers were introduced by Cantor in the late 19th century and problems arising from investigations of rules of arithmetic of cardinal numbers led to the birth of set theory. The operations of addition, multiplication and exponentiation of infinite cardinal numbers are a natural generalization of such operations on integers. Addition and multiplication of infinite cardinals turns out to be simple: when at least one of the numbers κ, λ is infinite then both κ + λ and κ·λ are equal to max {κ, λ}. In contrast with + and ·, exponentiation presents fundamental problems. In the simplest nontrivial case, 2κ represents the cardinal number of the power set P(κ), the set of all subsets of κ. (Here we adopt the usual convention of set theory that the number κ is identified with a set of cardinality κ, namely the set of all ordinal numbers smaller than κ.

§1. Introduction. The classical propositional calculus has an undeserved reputation among logicians as being essentially trivial. I hope to convince the reader that it presents some of the most challenging and intriguing problems in modern logic.

Although the problem of the complexity of propositional proofs is very natural, it has been investigated systematically only since the late 1960s. Interest in the problem arose from two fields connected with computers, automated theorem proving and computational complexity theory. The earliest paper in the subject is a ground-breaking article by Tseitin [62], the published version of a talk given in 1966 at a Leningrad seminar. In the three decades since that talk, substantial progress has been made in determining the relative complexity of proof systems, and in proving strong lower bounds for some restricted proof systems. However, major problems remain to challenge researchers.

The present paper provides a survey of the field, and of some of the techniques that have proved successful in deriving lower bounds on the complexity of proofs. A major area only touched upon here is the proof theory of bounded arithmetic and its relation to the complexity of propositional proofs. The reader is referred to the book by Buss [10] for background in bounded arithmetic. The forthcoming book by Krajíček [40] also gives a good introduction to bounded arithmetic, as well as covering most of the basic results in complexity of propositional proofs.

§1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of -analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to -formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated -comprehension, e.g., -comprehension. The details will be laid out in [28].

Ordinal-theoretic proof theory came into existence in 1936, springing forth from Gentzen's head in the course of his consistency proof of arithmetic. Gentzen fostered hopes that with sufficiently large constructive ordinals one could establish the consistency of analysis, i.e., Z2. Considerable progress has been made in proof theory since Gentzen's tragic death on August 4th, 1945, but an ordinal analysis of Z2 is still something to be sought. However, for reasons that cannot be explained here, -comprehension appears to be the main stumbling block on the road to understanding full comprehension, giving hope for an ordinal analysis of Z2 in the foreseeable future.

Roughly speaking, ordinally informative proof theory attaches ordinals in a recursive representation system to proofs in a given formal system; transformations on proofs to certain canonical forms are then partially mirrored by operations on the associated ordinals. Among other things, ordinal analysis of a formal system serves to characterize its provably recursive ordinals, functions and functionals and can yield both conservation and combinatorial independence results.