Solution of a Problem of Barendregt on Sensible lambda-Theories

Abstract

<i>H</i> is the theory extending &#946;-conversion by identifying all closed unsolvables. <i>H</i>&#969; is the closure of this theory under the &#969;-rule (and &#946;-conversion). A long-standing conjecture of H. Barendregt states that the provable equations of <i>H</i>&#969; form &#928;₁¹-complete set. Here we prove that conjecture.

17 pages

Cited by in corpus (2)

• The Omega Rule is ${\mathbf{\Pi }}_1^1$-Complete in the $\lambda \beta$-Calculus
• Addressing Machines as models of lambda-calculus