A note on indicator-functions
HTML articles powered by AMS MathViewer
- by J. Myhill PDF
- Proc. Amer. Math. Soc. 39 (1973), 181-183 Request permission
Abstract:
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.References
-
J. Myhill, Some properties of intuitionistic Zermelo-Frankel set-theory, Proceedings of the Logic Conference at Cambridge, August 1971.
Additional Information
- © Copyright 1973 American Mathematical Society
- Journal: Proc. Amer. Math. Soc. 39 (1973), 181-183
- MSC: Primary 02C15; Secondary 02K05
- DOI: https://doi.org/10.1090/S0002-9939-1973-0432406-2
- MathSciNet review: 0432406