Is $\Gamma \vdash x x : T$ possible in the simply typed lambda calculus?

Is $\Gamma \vdash x x : T$ possible?

This problem appears on page 104 of Benjamin Pierce's "Types and Programming Languages".

My conclusion is that it is was the case then we would get $x: T_1 \to T_2$ and $x: T_1$ and by some axiom, these types are not equal.

The problem is identifying this axiom but I fear it might be possible to have this equality...

Any hints?

You are on the right track. The argument you would use is on the lines of
size of types defined below: (I am assuming you are in the world of simply typed $\lambda$-calculus)

$size(T) = 1$

$size(T \to T') = size(T) + size(T')$

Unification will only work if the size of types is equal, and in this case
$size(T \to T') > size(T)$ hence there cannot be such a term.

However, if you add recursion/non-termination in the type system.
You can indeed have such a term.
$ \vdash (\lambda x. x x) (\lambda x. x x):\bot$

$\bot$ is the type that represents non-termination.

StackExchange Computer Science Q#115308, answer score: 2