×

zbMATH — the first resource for mathematics

Typed lambda-calculus in classical Zermelo-Fraenkel set theory. (English) Zbl 0990.03008
In this paper the author introduces “\(\text{ZF}_\varepsilon\) set theory” which, he claims, includes all of ZF + AF. However, his proof of the substitutivity for equality is not complete, so it is not clear whether his claim is justified. He then develops \(\text{ZF}_\varepsilon\) set theory within a classical extension of lambda calculus.

MSC:
03B40 Combinatory logic and lambda calculus
03E40 Other aspects of forcing and Boolean-valued models
68N18 Functional programming and lambda calculus
PDF BibTeX XML Cite
Full Text: DOI