The systems of cumulative logic treated in this book are introduced as generalisations and at the same time as extensions of the simple theory of types predication is taken to be cumulative in the sense that objects of a fixed type may be predicated of objects with arbitrary lower types, and not only, as in the case of normal simple type theory, of objects having the immediately preceding type. Formal systems of the Gentzen-sequence sort are established with appropriately generalised quantification and abstraction rules. NO cumulative logic satisfies Gentzen's Hauptsatz (the cut-elimination theorem) But completeness theorems with respect to 5 suitable semantic can be proved. Since the type-homogenous membership relation ( of set theory can he defined in terms of cumulative predication, certain element extensions of the ,pure' Systems of cumulative logic lend themselves to the formalisation of set theory. There are natural extensions of this sort in which Zermelo's set theory can be deduced. The consistency of these Systems is proved and decidability problems are considered At the end of the book, a special system of cumulative logic is set up with close connections to Frege's System in his Grundgesetze der Arithmetik on the one hand, and to Quine's New Foundations on the other. The presentation is broad enough for the book to serve as an introduction to proof theory and to the model theory of type-logics. For example, a semantic proof of the cut-elimination theorem for simple type-theory (following Prawitz) has been included. Of interest to: Logicians, mathematicians, philosophers and historians of these disciplinesweiterlesen