On the Computability of the Fan Functional

  • Dag Normann
  • William Tait
Part of the Outstanding Contributions to Logic book series (OCTR, volume 13)


We give a self-contained presentation of the original argument for why the fan functional is countably recursive, but not Kleene computable. This proof, from 1958, is due to the second author and has not been published before. A lemma concerning the Kleene computable functionals used in the proof is unnecessarily strong, which is fortunate since there is a counterexample, due to the first author, which we include.


Fan functional Recursively countable Kleene computable 

Mathematics subject classification:



  1. 1.
    Escardó, M.H.: Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics. J. Symb. Log. 78(3), 764–784 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Feferman, S.: Recursion in total functionals of finite type. Compos. Math. 35, 3–22 (1977)MathSciNetzbMATHGoogle Scholar
  3. 3.
    Gandy, R.O., Hyland, J.M.E.: Computable and recursively countable functions of higher type. In: Gandy, R.O., Hyland, J.M.E. (eds.) Logic Colloquium ’76, pp. 407–438. North Holland, Amsterdam (1977)Google Scholar
  4. 4.
    Gödel, K.: The present situation in the foundations of mathematics (1933). Collected Works, vol. III, pp. 45–53. Oxford University Press, Oxford (1995)Google Scholar
  5. 5.
    Gödel, K.: Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12, 280–287 (1958). Reprinted with an English translation in Gödel [7]. Gödel [6] is a revised versionGoogle Scholar
  6. 6.
    Gödel, K.: On an extension of finitary mathematics which has not yet been used (1972) in [7], pp. 271–289 (1990)Google Scholar
  7. 7.
    Gödel, K.: Collected Works, vol. II. Oxford University Press, Oxford (1990)zbMATHGoogle Scholar
  8. 8.
    Harrison, J.: Equivalence of the effective operations and the hereditarily continuous functionals. In: Stanford Seminar Report, pp. 204–206 (1963). Appendix C to Tait [17]Google Scholar
  9. 9.
    Kleene, S.C.: Recursive functionals and quantifiers of finite type I. Trans. Am. Math. Soc. 91, 1–52 (1959)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Kleene, S.C.: Countable functionals. In: Heyting, A. (ed.) Constructivity in Mathematics: Proceedings of the Colloquium held at Amsterdam 1957, pp. 81–100. North-Holland, Amsterdam (1959)Google Scholar
  11. 11.
    Kreisel, G.: Lecture notes from a course on Constructive Mathematics, Stanford University (1958, 1959)Google Scholar
  12. 12.
    Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. In: Heyting, A. (ed.) Constructivity in Mathematics: Proceedings of the Colloquium held at Amsterdam 1957, pp. 101–128. North-Holland, Amsterdam (1959)Google Scholar
  13. 13.
    Longley, J.R., Normann, D.: Higher Order Computability. Springer, Berlin (2015)CrossRefzbMATHGoogle Scholar
  14. 14.
    Normann, D.: Recursion on the Countable Functionals. Springer, Berlin (1980)CrossRefzbMATHGoogle Scholar
  15. 15.
    Normann, D.: The continuous functionals. In: Griffor, E.R. (ed.) Handbook of Computability Theory, pp. 251–275. Elsevier, Amsterdam (1999)CrossRefGoogle Scholar
  16. 16.
    Tait, W.W.: Continuity Properties of Partial Recursive Functionals of Finite Type, International Congress for Logic, Methodology and Philosophy of Science: Abstracts of contributed papers. Stanford University, Stanford, California (1960)Google Scholar
  17. 17.
    Tait, W.W.: A second order theory of functionals of higher type, with two appendices. Appendix A: Intensional functionals. Appendix B: An interpretation of functionals by convertible terms. Stanford Seminar Report, pp. 171–206 (1963). Unpublished. A published version is Tait [18]Google Scholar
  18. 18.
    Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symb. Log. 32, 198–212 (1967)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2017

Authors and Affiliations

  1. 1.Department of MathematicsThe University of OsloOsloNorway
  2. 2.ChicagoUSA

Personalised recommendations