  As we saw above, the distinction: objects, predicates, predicate of predicates, etc., seems enough to block Russell’s paradox (and this was recognised by Chwistek and Ramsey). We first describe the type structure as it is in Principia and later in this section we present the elegant formulation due to Church 1940 based on \(\lambda\)-calculus. The types can be defined as