Separating the Fan Theorem and Its Weakenings II

  • Robert S. LubarskyEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


Varieties of the Fan Theorem have recently been developed in reverse constructive mathematics, corresponding to different continuity principles. They form a natural implicational hierarchy. Earlier work showed all of these implications to be strict. Here we re-prove one of the strictness results, using very different arguments. The technique used is a mixture of realizability, forcing in the guise of Heyting-valued models, and Kripke models.


Fan Theorems Kripke models Forcing Heyting-valued models Formal topology Recursive realizability 

AMS 2010 MSC

03C90 03E70 03F50 03F60 03D80 


  1. 1.
    Beeson, M.: Foundations of Constructive Mathematics. Springer, Heidelberg (1985)CrossRefzbMATHGoogle Scholar
  2. 2.
    Berger, J.: The logical strength of the uniform continuity theorem. In: Beckmann, A., Berger, U., Löwe, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol. 3988, pp. 35–39. Springer, Heidelberg (2006). CrossRefGoogle Scholar
  3. 3.
    Berger, J.: A separation result for varieties of Brouwer’s Fan Theorem. In: Proceedings of the 10th Asian Logic Conference (ALC 10), Kobe University in Kobe, Hyogo, Japan, 1–6 September 2008, pp. 85–92 (2010)Google Scholar
  4. 4.
    Diener, H., Loeb, I.: Sequences of real functions on [0, 1] in constructive reverse mathematics. Ann. Pure Appl. Logic 157(1), 50–61 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Diener, H., Lubarsky, R.: Notions of cauchyness and metastability. In: Artemov, S., Nerode, A. (eds.) Symposium on Logical Foundations in Computer Science 2018, LNCS. Springer, Heidelberg (2018, to appear)Google Scholar
  6. 6.
    Fourman, M.P., Hyland, J.M.E.: Sheaf models for analysis. In: Fourman, M., Mulvey, C., Scott, D. (eds.) Applications of Sheaves. LNM, vol. 753, pp. 280–301. Springer, Heidelberg (1979). CrossRefGoogle Scholar
  7. 7.
    Fourman, M.P., Scott, D.S.: Sheaves and logic. In: Fourman, M., Mulvey, C., Scott, D. (eds.) Applications of Sheaves. LNM, vol. 753, pp. 302–401. Springer, Heidelberg (1979). CrossRefGoogle Scholar
  8. 8.
    Gambino, N.: Heyting-valued interpretations for Constructive Set Theory. Ann. Pure Appl. Logic 137, 164–188 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Julian, W., Richman, F.: A uniformly continuous function on [0,1] that is everywhere different from its infimum. Pac. J. Math. 111(2), 333–340 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Lubarsky, R., Diener, H.: Separating the Fan Theorem and its weakenings. J. Symbolic Logic 79, 792–813 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    van Oosten, J.: Realizability: An Introduction to its Categorical Side. Elsevier, Amsterdam (2008)zbMATHGoogle Scholar
  12. 12.
    Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, Vol. 2. In: Studies in Logic, vol. 123, Elsevier (1988)Google Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.Department of Mathematical SciencesFlorida Atlantic UniversityBoca RatonUSA

Personalised recommendations