Remote Access Proceedings of the American Mathematical Society
Green Open Access

Proceedings of the American Mathematical Society

ISSN 1088-6826(online) ISSN 0002-9939(print)



A note on indicator-functions

Author: J. Myhill
Journal: Proc. Amer. Math. Soc. 39 (1973), 181-183
MSC: Primary 02C15; Secondary 02K05
MathSciNet review: 0432406
Full-text PDF Free Access

Abstract | References | Similar Articles | Additional Information

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 [Enhancements On Off] (What's this?)

  • [1] J. Myhill, Some properties of intuitionistic Zermelo-Frankel set-theory, Proceedings of the Logic Conference at Cambridge, August 1971.

Similar Articles

Retrieve articles in Proceedings of the American Mathematical Society with MSC: 02C15, 02K05

Retrieve articles in all journals with MSC: 02C15, 02K05

Additional Information

Keywords: Existence and disjunction-properties, realizability
Article copyright: © Copyright 1973 American Mathematical Society