Reducibility of types in typed lambda calculus. Comment on a paper by Richard Statman (Q1104311)

If types are built up from the base type 0 using the operation \(\to\), \(\sigma\leq \tau\) is defined by: \((\exists M)M\in \sigma \to \tau \wedge M closed\wedge (\forall N_ 1)(\forall N_ 2)N_ 1,N_ 2\in \sigma \wedge N_ 1, N_ 2\quad closed\to (N_ 1=_{\beta \eta}N_ 2\leftrightarrow MN_ 1=_{\beta \eta}MN_ 2).\sigma <\tau\) iff \(\sigma\leq \tau \wedge \sim \tau \leq \sigma\). \(\sigma\) equivalent to \(\tau\) iff \(\sigma\leq \tau \wedge \tau \leq \sigma.\) \textit{R. Statman} [On the existence of closed terms in typed \(\lambda\)- calculus, I, in: ``To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism'', 511-534 (1980; Zbl 0469.03006)] showed that the equivalence classes of these types are well ordered in type \(\omega +2\) or \(\omega +3.\) The current well written paper shows that type \(\omega +2:\) (((0\(\to 0)\to 0)\to 0)\to 0\to 0\) is strictly less than (0\(\to (0\to 0))\to 0\to 0\) which is the maximal type. Hence these equivalence classes are ordered in type \(\omega +3\).