 The above definition of the set of terms of type theory is sufficient to rule out terms such as \(xx\). Of course, ‘\(xx\)’ is not a typed term at all for the simple reason that no types have been assigned to it. What is meant is that there is no type \(\sigma\) that could be assigned to \(x\) such that ‘\(xx\)’ could be annotated in a legal way to make a typed term. We cannot assign to \(x\) a type variable, because then the type of the left-hand \(x\) would fail to be a function type (i.e., a type of the shape ‘\(\sigma \rightarrow \tau\)’). Moreover, we cannot assign to \(x\) a function type \(\sigma \rightarrow \tau\), because then then \(\sigma\) would be equal to \(\sigma \rightarrow \tau\), which is impossible.