  and an axiom scheme of comprehension at each type. Notice that the formula displayed above is not, strictly speaking, an axiom of extensionality, since the variables do not have concrete type subscripts, so it is not officially a formula at all. It’s a kind of axiom scheme. Annoyingly, this subtlety matters. The fact that variables have type subscripts precludes the more usual exploitations of subscripting for purposes such as indicating position in a sequence. This makes the language of type theory infeasible for most mathematical purposes, so one looks for excuses to omit the type subscripts. Why might this be a safe manœuvre? Let us define \(\Phi^+\) to be the result of raising all the type subscripts on all variables in \(\Phi\). It’s safe because the theory has the same axioms at each type, so it has the same theorems at each type, so whenever one has a proof of a formula \(\Phi\) one also has a proof of \(\Phi^+\). One omits the type subscripts because even though, once has omitted them, there are infinitely many ways of restoring them, these infinitely many differently restored versions do not appear to differ significantly. We shall take up later the theme of the significance of this difference, but for the moment we note only that it appears – as it appeared to Russell and his successors up to and including Quine – that the differences could be safely overlooked. This strategy of overlooking is called typical ambiguity.