The existence of an ω2-Souslin tree will be proved (Theorem 2.2 or §3) from the Generalized Continuum Hypothesis (GCH) plus Jensen's combinatorial principle □ω1. Thus, it follows from Jensen's 1.4(2) that the consistency of the formal theory T given by ZFC + GCH + “ω2-Souslin Hypothesis” implies the consistency of ZFC + “there exists a Mahlo cardinal.” So one does not hope to prove the consistency of this T relative to the consistency of ZFC + “there is an inaccessible cardinal, hence there are transitive models of ZFC.”

Silver [5, Theorem 5.8] has shown that the consistency of ZFC + “there is a weakly compact cardinal” implies the consistency of ZFC + not GCH + “there is no ω2-Aronszajn tree, hence no ω2-Souslin tree”; this is one reason why we deal with GCH here. Jensen has shown that the consistency of ZFC implies the consistency of ZFC +GCH + “ω1-Souslin Hypothesis.”

In the preliminary §1, we state some definitions and known results about trees and some of Jensen's combinatorial principles, including □ and ◇*(E).

Our main Lemma 2.1 states (a fortiori) that GCH implies ◇* at ω-cofinal elements of ω2 (i.e., in our notation, ◇*(E(ω) ∩ ω2)). From Lemma 2.1 and the known facts of §1, it is proved (2.5) that if □ k , the cofinality cf(k)> ω, and GCH, then there is a k +-Souslin tree. For k = ω1, this implies the result mentioned above for ω2-Souslin trees.