Systeme der kumulativen Logik

The systems of cumulative logic in this work are presented as generalizations and extensions of the simple theory of types. Predication is cumulative, allowing objects of a fixed type to be predicated of objects with arbitrary lower types, unlike normal simple type theory, which restricts this to immediately preceding types. Formal systems of the Gentzen-sequence type are established with generalized quantification and abstraction rules. While no cumulative logic satisfies Gentzen's Hauptsatz (cut-elimination theorem), completeness theorems can be proven concerning suitable semantics. The type-homogeneous membership relation from set theory can be defined using cumulative predication, leading to certain element extensions of pure cumulative logic that facilitate the formalization of set theory, including natural extensions from which Zermelo's set theory can be deduced. The consistency of these systems is demonstrated, and decidability issues are addressed. The book concludes with a special system of cumulative logic that connects closely to Frege's system in his Grundgesetze der Arithmetik and Quine's New Foundations. The presentation is comprehensive enough to serve as an introduction to proof theory and model theory of type-logics, including a semantic proof of the cut-elimination theorem for simple type theory. It will interest logicians, mathematicians, philosophers, and historians of these fields.