The omega rule is Π 1 1 -complete in the λβ-calculus
We give a many-one reduction of the set of true Π11 sentences to the set of consequences of the λ-calculus with the ω-rule. This solves in the affirmative a long-standing problem of H. Barendregt (1975).