 raises worries that paradox may emerge. Church thought that eschewing the use of free variables and restricting excluded middle (Church, 1932: 346–7) blocked paradox but Kleene and Rosser showed (1935), using a strategy based on Richard’s paradox, that the system was trivial: every formula could be derived using the rules. Church fixed this up to produce a consistent untyped \(\lambda\) calculus, but the important step with regard to the CH correspondence was the development of typed \(\lambda\) calculi.