Proving that $\Omega = (\lambda x.xx)(\lambda x.xx)$ is not typable in the simply typed lambda calculus

Question

I am trying to prove that $\Omega = (\lambda x.xx)(\lambda x.xx)$ is not typable in the simply typed lambda calculus. Surprisingly, different textbooks and lecture notes do not contain that proof, please correct me if I am wrong.

The proof is important, because $\Omega$ does not have a normal form and if it cannot be typed then normalisation theorems do not apply.

From the book Proofs and Types by Girard, Taylor, and Lafont, I read:

If $t$ and $u$ are terms respectively $U \rightarrow V$ and $U$, then $t \; u$ is a term of type $V$.

I am going to prove that any lambda term of type $x \; x$ cannot be typed.

Suppose that the type of the latter $x$ is $T$, then the type of the former $x$ should be $T \rightarrow U$.

That is impossible, because $x$ cannot have two different types.

This implies that $\Omega$ is not typable in the simply typed lambda calculus, because it contains an expression of the form $x\; x$.

My questions are:

1. Is my proof correct?
2. Is there a better proof?
3. Does there exist some extension of lambda calculus where $\Omega$ can be typed?

Answer 1

1. Yes.
2. I do not think so. You got the essence of the incompatibility.
3. Yes. The most notable example employs intersection-types which allow, following the example of your choice, assignments like $$x\ \ :\ \ T\ \wedge\ T\!\rightarrow\!U$$ and, consequently $$x x\ \ :\ \ U$$ and $$\lambda x.xx\ \ :\ \ T\!\rightarrow\!U \wedge T\!\rightarrow\!U$$ More details expressed in an introductive form can be found, among the many others, in the 1998 article titled Intersection Types, $\lambda$-models, and Bohm Trees, by M. Dezani-Ciancaglini, E. Giovannetti, and U. De'Liguoro.