Hostname: page-component-586b7cd67f-t7fkt Total loading time: 0 Render date: 2024-11-29T19:10:32.331Z Has data issue: false hasContentIssue false

Relative computability in the effective topos

Published online by Cambridge University Press:  24 October 2008

Wesley Phoa
Affiliation:
Department of Pure Mathematics and Mathematical Statistics, 16 Mill Lane, Cambridge CB2 1SB

Extract

Let ℕ be the natural numbers object in , the effective topos. It was shown in [1] that the maps ℕ → ℕ are (internally or externally) just the total recursive functions. Now a subset A ⊆ ω of natural numbers corresponds to a ¬¬-closed subobject A ↣ ℕ; let kA be the least topology forcing A to be decidable, and let ℕA be the sheafification of ℕ with respect to this topology. Then one would expect the maps ℕ → ℕA to be the total functions recursive in A.

Type
Research Article
Copyright
Copyright © Cambridge Philosophical Society 1989

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Hyland, J. M. E.. The effective topos. In The L. E. J. Brouwer Centenary Symposium (ed. Troelstra, A. S. and Van Dalen, D.) (North-Holland, 1982).Google Scholar
[2]Hyland, J. M. E., Johnstone, P. T. and Pitts, A. M.. Tripos theory. Math. Proc. Cambridge Philos. Soc. 88 (1980), 205231.CrossRefGoogle Scholar
[3]Hyland, J. M. E., Robinson, E. and Rosolini, G.. Discrete objects in the effective topos. (Preprint.)Google Scholar
[4]Pitts, A. M.. The theory of triposes. Ph.D. thesis, University of Cambridge (1981).Google Scholar