An Unsolvable Numeral System in lambda Calculus

Abstract

Abstract For numeral systems in untyped λ-calculus the definability of a successor, a predecessor and a test for zero implies the definability of all recursive functions on that system. Towards a disproof of the converse statement, H. P. Barendregt and the author constructed a numeral system consisting of unsolvable λ-terms, being adequate for unary functions. Then, independently, B. Intrigila found an analogous system for all computable functions.