Hostname: page-component-78c5997874-fbnjt Total loading time: 0 Render date: 2024-11-13T07:06:45.580Z Has data issue: false hasContentIssue false
  • English
  • Français

Church's thesis, continuity, and set theory

Published online by Cambridge University Press:  12 March 2014

M. Beeson  and
A. Ščedrov
M. Beeson*
Affiliation:
Rijksuniversiteit Utrecht
A. Ščedrov
Affiliation:
Utrecht, State University of New YorkBuffalo, New York 14214
*
Department of Mathematics and Computer Science, San Jose State University, San Jose, California 95192
Get access Rights & Permissions [Opens in a new window]

Abstract

Under the assumption that all “rules” are recursive (ECT) the statement Cont(NN, N) that all functions from NN to N are continuous becomes equivalent to a statement KLS in the language of arithmetic about “effective operations”. Our main result is that KLS is underivable in intuitionistic Zermelo-Fraenkel set theory + ECT. Similar results apply for functions from R to R and from 2N to N. Such results were known for weaker theories, e.g. HA and HAS. We extend not only the theorem but the method, fp-realizability, to intuitionistic ZF.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 49 , Issue 2 , June 1984 , pp. 630 - 643
Copyright
Copyright © Association for Symbolic Logic 1984

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

[Bl]Beeson, M., The nonderivability in intuitionistic formai systems of theorems on the continuity of effective operations, this Journal, vol. 40 (1975), pp. 321–346.Google Scholar
[B2]Beeson, M., The unprovability in intuitionistic formal systems of the continuity of effective operations on the reals, this Journal, vol. 41 (1976), pp. 18–24.Google Scholar
[B3]Beeson, M., Continuity and comprehension in intuitionistic formal systems, Pacific Journal of Mathematics, vol. 68 (1977), pp. 29–40.CrossRefGoogle Scholar
[B4]Beeson, M., Continuity in intuitionistic set theories, Logic Colloquium '78 (Boffa, M., van Dalen, D. and McAloon, K., editors), North-Holland, Amsterdam, 1979, pp. 1–52.Google Scholar
[B5]Beeson, M., Recursive models for constructive set theories, Annals of Mathematical Logic, vol. 23 (1982), pp. 127–178.CrossRefGoogle Scholar
[D]Diaconescu, R., Axiom of choice and ocomplementation, Proceedings of the American Mathematical Society, vol. 51 (1975), pp. 176–178.CrossRefGoogle Scholar
[G]Goodman, N. D., A genuinely intensional set theory, Intensionalmathematics (Shapiro, S., editor), North-Holland, Amsterdam (to appear).Google Scholar
[K]Kušner, B. A., Lectures on constructive mathematical analysis, “Nauka”, Moscow, 1973. (Russian)Google Scholar
[KLS]Kreisel, G., Lacombe, D. and Shoenfield, J. R., Partial recursive functional and effective operations, Constructivity in mathematics (Proceedings of the colloquium held at Amsterdam, 1957) (Heyting, A., editor), North-Holland, Amsterdam, 1959, pp. 290–297.Google Scholar
[M1]Myhill, J., Some properties of intuitionistic Zermelo-Frankel set theory, Cambridge Summer School in Mathematical Logic (held in Cambridge, England, August, 1971) (Mathias, A. and Rogers, H., editors), Lecture Notes in Mathematics, vol. 337, Springer-Verlag, Berlin, 1973, pp. 206–231.CrossRefGoogle Scholar
[M2]Myhill, J., Constructive set theory, this Journal, vol. 40 (1975), pp. 347–382.Google Scholar
[T]Troelstra, A. S. (editor), Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin, 1973.CrossRefGoogle Scholar
[V]Visser, A., On the completeness principle: a study of provability in Heyting's arithmetic and extensions, Annals of Mathematical Logic, vol. 22 (1982), pp. 263–295.CrossRefGoogle Scholar