We give a formalization of the ramified type theory as described in the PrincipiaMathematica, trying to keep it as close as possible to the ideas of the Principia. As an alternative, distancing ourselves from the Principia, we express notions from the ramified type theory in a lambda calculus style, thus clarifying the type system in a contemporary setting. Both formalizations are inspired by current developments in research on type theory and typed lambda calculus. In these formalizations, and also when defining 'truth', we will need the notion of substitution. As substitution is not formally defined in the Principia, we have to define it ourselves.
展开▼
