Solution of a Problem of Barendregt on Sensible lambda-Theories
classification
💻 cs.LO
keywords
barendregtconjectureconversiontheoryclosedclosurecompleteequations
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.