William W. Tait

The reduction of the lambda calculus to the theory of combinators in [Sch¨ onfinkel, 1924] applies to positive implicational logic, i.e. to the typed lambda calculus, where the types are built up from atomic types by means of the operation A −→ B, to show that the lambda operator can be eliminated in favor of combinators K and S of each type A −→ (B −→ A) and (A −→ (B −→ C)) −→ ((A −→ B) −→ (A −→ C)), respectively.1 I will extend that result to the case in which the types are built up by means of the general function type ∀x : A.B(x) as well as the disjoint union type ∃x : A.B(x)– essentially to the theory of [Howard, 1980]. To extend the treatment of −→ to ∀ we shall need a generalized form of the combinators K and S, and to deal with ∃ we will need to introduce a new form of the combinator S..

Foundations of a General Theory of Manifolds [Cantor, 1883], which I will refer to as the Grundlagen, is Cantor’s first work on the general theory of sets. It was a separate printing, with a preface and some footnotes added, of the fifth in a series of six papers under the title of “On infinite linear point manifolds”. I want to briefly describe some of the achievements of this great work. But at the same time, I want to discuss its connection with the so-called paradoxes in set theory. There seems to be some agreement now that Cantor’s own understanding of the theory of transfinite numbers in that monograph did not contain an implicit contradiction; but there is less agreement about exactly why this is so and about the content of the theory itself. For various reasons, both historical and internal, the Grundlagen seems not to have been widely read compared to later works of Cantor, and to have been even less well understood. But even some of the more recent discussions of the work, while recognizing to some degree its unique character, misunderstand it on crucial points and fail to convey its true worth.