 Example 5 Suppose we omit the use of type symbols in the definitions of wffs. Then we can write the formula \(\lambda x\nsim[xx]\), which we shall call \(\textrm{R}\). It can be regarded as denoting the set of all sets x such that x is not in x. We may then consider the formula \([\textrm{R R}]\), which expresses the assertion that \(\textrm{R}\) is in itself. We can clearly prove \([\textrm{R R}] \equiv [[\lambda x\nsim [xx]] \textrm{R}]\), so by λ-conversion we can derive \([\textrm{R R}] \equiv\, \nsim[\textrm{R R}]\), which is a contradiction. This is Russell’s paradox. Russell’s discovery of this paradox (Russell 1903, 101-107) played a crucial role in the development of type theory. Of course, when type symbols are present, \(\textrm{R}\) is not well-formed, and the contradiction cannot be derived.