We provide a syntax and a derivation system fora formal language of mathematics called Weak Type Theory (WTT). We give the metatheory of WTT and a number of illustrative examples.WTT is a refinement of de Bruijn''s Mathematical Vernacular (MV) and hence:– WTT is faithful to the mathematician''s language yet isformal and avoids ambiguities.

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)

Typed λ-calculus uses two abstraction symbols which are usually treated in different ways: λx:*.x has as type the abstraction Πx:*.*, yet Πx:*.* has type □ rather than an abstraction; moreover, C is allowed and β-reduction evaluates it, but C is rarely allowed. Furthermore, there is a general consensus that λ and Π are different abstraction operators. While we agree with this general consensus, we find it nonetheless important to allow Π to act as an abstraction operator. Moreover, experience with AUTOMATH (...) and the recent revivals of Π-reduction as in [11, 14], illustrate the elegance of giving Π-redexes a status similar to λ-redexes. However, Π-reduction in the λ-cube faces serious problems as shown in [11, 14]: it is not safe as regards subject reduction, it does not satisfy type correctness, it loses the property that the type of an expression is well-formed and it fails to make any expression that contains a Π-redex well-formed. In this paper, we propose a solution to all those problems. The solution is to use a concept that is heavily present in most implementations of programming languages and theorem provers: abbreviations or let-expressions. We will show that the λ-cube extended with Π-conversion and abbreviations satisfies all the desirable properties of the cube and does not face any of the serious problems of Π-reduction. We believe that this extension of the λ-cube is very useful: it gives a full formal study of two concepts that are useful for theorem proving and programming languages. (shrink)

In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 1910-1912) and Church's simply typed λ-calculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating on Frege's (...) Grundgesetze der Arithmetik for which Russell applied his famous paradox and this led him to introduce the first theory of types, the Ramified Type Theory (RTT). We present RTT formally using the modern notation for type theory and we discuss how Ramsey, Hilbert and Ackermann removed the orders from RTT leading to the simple theory of types STT. We present STT and Church's own simply typed λ-calculus (λ → C) and we finish by comparing RTT, STT and λ → C. (shrink)