The omega rule is \Pi^1_1-complete in the lambda-calculus
Benedetto Intrigila, Rick Statman · Cineca Institutional Research Information System (Tor Vergata University) · 2007
We give a many-one reduction of the set of true \Pi^1_1 sentences to the set of consequences of the lambda-calculus with the omega-rule. This solves in the affirmative a long-standing problem of H. Barendregt (1975). © Springer-Verlag Berlin Heidelberg 2007.