$$(abst) \:\frac{\Gamma, x: t_1 \vdash t_2: t_3 \quad \Gamma \vdash (x: t_1) \to t_3: s}{\Gamma \vdash (x: t_1. t_2): (x: t_1) \to t_3}$$
In this rule, why is $(x: t_1) \to t_3$ required to be an inhabitant of some sort? Isn't assuming $t_1: s$ enough?
There are two issues here.
The first most obvious one, is that if there is no rule $(s_1,s_2,s)$ in the pure type system, then there is no way to get from the hypotheses $$ \Gamma \vdash t_1:s_1$$ and $$ \Gamma, x:t_1\vdash t_3:s_2$$ to the conclusion $$ \Gamma\vdash (x:t_1)\rightarrow t_3 : s$$ You can see that if there is no such rule, then your hypothesis is insufficient for forming the product type, and therefore you shouldn't be able to form terms of that type. Note that in the Calculus of Constructions, any $s_1, s_2$ has a corresponding $s$ ($=s_2$), so the premisses are sufficient for the conclusion in all cases.
Another, more subtle issue is that even the fact $\Gamma, x:t_1\vdash t_3:s_2$ for some $s_2$ is not obvious from the fact $$\Gamma, x:t_1\vdash t_2:t_3 $$ While actually true, this fact can be subtle to prove depending on how you set up your rules.
The rule you give minimizes the hassle, as it gives you directly the hypothesis that the product is well-formed without having to prove it after the fact.
