A note on indicator-functions
John R. Myhill · Proceedings of the American Mathematical Society · 1973
A system has the existence-property for abstracts (existence property for numbers, disjunction-property) if whenever $\vdash (\exists x)A(x), \vdash A({\text {t}})$ for some abstract $({\text {t}})( \vdash A(n)$ for some numeral $n$; if whenever $\vdash A \vee B, \vdash A$ or $\vdash B.(\exists x)A(x),A,B$ are closed). We show that the existence-property for numbers and the disjunction property are never provable in the system itself; more strongly, the (classically) recursive functions that encode these properties are not provably recursive functions of the system. It is however possible for a system (e.g., ${\mathbf {ZF}} + V = L$) to prove the existence-property for abstracts for itself.