Here, the author, develops a type theory, studies its properties, and explains its uses in applications to computer science. In particular, type theory is shown to offer a powerful and uniform language for programming, program specification and development, and logical reasoning.

The paper first formalizes the ramified type theory as (informally) described in the Principia Mathematica [32]. This formalization is close to the ideas of the Principia, but also meets contemporary requirements on formality and accuracy, and therefore is a new supply to the known literature on the Principia (like [25], [19], [6] and [7]).As an alternative, notions from the ramified type theory are expressed in a lambda calculus style. This situates the type system of Russell and Whitehead in a modern (...) setting. Both formalizations are inspired by current developments in research on type theory and typed lambda calculus; see [3]. (shrink)

A formal theory of truth, alternative to tarski's 'orthodox' theory, based on truth-value gaps, is presented. the theory is proposed as a fairly plausible model for natural language and as one which allows rigorous definitions to be given for various intuitive concepts, such as those of 'grounded' and 'paradoxical' sentences.

Both in Kripke's Theory of Truth KTT [8] and Russell's Ramified Type Theory RTT [16, 9] we are confronted with some hierarchy. In RTT, we have a double hierarchy of orders and types. That is, the class of propositions is divided into different orders where a propositional function can only depend on objects of lower orders and types. Kripke on the other hand, has a ladder of languages where the truth of a proposition in language Ln can only be made (...) in Lm where m)n. Kripke finds a fixed point for his hierarchy . We investigate in this paper the similarities of both hierarchies: At level n of KTT the truth or falsehood of all order-n-propositions of RTT can be established. Moreover, there are order-n-propositions that get a truth value at an earlier stage in KTT. Furthermore, we show that wrr is more restrictive than KTT, as some type restrictions are not needed in KTT and more formula., can be expressed in the latter.Looking back at the double hierarchy of Russell, Ramsey [11] and Hilbert and Ackermann [7] considered the orders to cause the restrictiveness, and therefore removed them. This removal resulted in Church's Simple Type Theory STT [1] We show however that orders in RTT correspond to levels of truth in KTT. Hence, KTT can be regarded as the dual of STT where types have been removed and orders are maintained. As RTT is more restrictive than KTT, we can conclude that it is the combination of types and orders that was the restrictive factor in RTT. (shrink)

This paper is divided into two parts. Part I provides a resumé of the evolution of the notion of predicativity. Part II describes our own work on the subject.Part I§1. Conceptions of sets.Statements about sets lie at the heart of most modern attempts to systematize all (or, at least, all known) mathematics. Technical and philosophical discussions concerning such systematizations and the underlying conceptions have thus occupied a considerable portion of the literature on the foundations of mathematics.

Gathered together here are the fundamental texts of the great classical period in modern logic. A complete translation of Gottlob Frege's Begriffsschrift--which opened a great epoch in the history of logic by fully presenting propositional calculus and quantification theory--begins the volume, which concludes with papers by Herbrand and by Gödel.