Summary A λ-theory T is a consistent set of equations between λ-terms closed under derivability. The degree of T is the degree of the set of Gödel numbers of its elements. is the λ-theory axiomatized by the set { M = N ∣ M, N unsolvable}. A λ-theory is sensible iff T ⊃ ; for a motivation see [6] and [4]. In §1 it is proved that the theory is Σ 2 0 -complete. We present Wadsworth's proof that its unique maximal consistent extension * (= Th( D ∞ )) is Π 2 0 -complete. In §2 it is proved that η (= λη-calculus + ) is not closed under the ω-rule (see [1]). In §3 arguments are given to conjecture that is Π 1 1 -complete. This is done by representing recursive sets of sequence numbers as λ-terms and by connecting wellfoundedness of trees with provability in ω. In §4 an infinite set of equations independent over η will be constructed. From this it follows that there are 2 ℵ 0 sensible theories T such that and 2 ℵ 0 sensible hard models of arbitrarily high degrees. In §5 some nonprovability results needed in §§1 and 2 are established. For this purpose one uses the theory η 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.

§ 1 is concerned with the term model of the α-calculus. It is proved that Church's δ is not dofinable and that the definable functions into the numerals are constant. In § 2 it is proved that for several α-algebras the range of a representable function is either a singleton or infinite. In § 3 it is examined in which α-algebras the local representability of external functions implies the global representability.