Solution of a Problem of Barendregt on Sensible lambda-Theories
Logic in Computer Science
2017-01-11 v2
Abstract
<i>H</i> is the theory extending β-conversion by identifying all closed unsolvables. <i>H</i>ω is the closure of this theory under the ω-rule (and β-conversion). A long-standing conjecture of H. Barendregt states that the provable equations of <i>H</i>ω form Π<sub>1</sub><sup>1</sup>-complete set. Here we prove that conjecture.
Keywords
Cite
@article{arxiv.cs/0609080,
title = {Solution of a Problem of Barendregt on Sensible lambda-Theories},
author = {Benedetto Intrigila and Richard Statman},
journal= {arXiv preprint arXiv:cs/0609080},
year = {2017}
}
Comments
17 pages