A $\lambda$-theory $T$ is a consistent set of equations between $\lambda$-terms closed under derivability. The degree of $T$ is the degree of the set of Godel numbers of its elements. $\mathscr{H}$ is the $\lamda$-theory axiomatized by the set $\{M = N \mid M, N \text{unsolvable}$. A $\lamda$-theory is sensible $\operatorname{iff} T \supset \mathscr{H}$, for a motivation see [6] and [4]. In $\S$ it is proved that the theory $\mathscr{H}$ is $\sum^0_2$-complete. We present Wadsworth's proof that its unique maximal consistent extention $\mathscr{H}^\ast ( = \mathrm{T}(D_\infty))$ is $\Pi^0_2$-complete. In $\S2$ it is proved that $\mathscr{H}_\eta( = \lambda_\eta-\text{Calculus} + \mathscr{H})$ is not closed under the $\omega$-rule (see [1]). In $\S3$ arguments are given to conjecture that $\mathscr{H}\omega ( = \lambda + \mathscr{H} + omega-rule)$ is $\Pi^1_1$-complete. This is done by representing recursive sets of sequence numbers as $\lambda$-terms and by connecting wellfoundedness of trees with provability in $\mathscr{H}\omega$. In $\S4$ an infinite set of equations independent over $\mathscr{H}_\eta$ will be constructed. From this it follows that there are $2^{\aleph_0$ sensible theories $T$ such that $\mathscr{H} \subset T \subset \mathscr{H}^\ast$ and $2^\aleph_0$ sensible hard models of arbitrarily high degrees. In $\S5$ some nonprovability results needed in $\S\S1$ and 2 are established. For this purpose one uses the theory $\mathscr{H}_\eta$ extended with a reduction relation for which the Church-Rosser theorem holds. The concept of Gross reduction is used in order to show that certain terms have no common reduct.