Skip to main content
SpringerLink
Log in

Feferman on Computability

  • Chapter
  • First Online:
Feferman on Foundations

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 13))

  • 702 Accesses

Abstract

Solomon Feferman has left his mark on computability theory, as on many other areas of foundational studies. The purpose of this paper is, by means of reviewing a selected few of his many papers in this area, to give an idea of his impressive insights and developments in this field.

To the memory of Sol Feferman, who, with his unfailing kindness, patience and good humour, was a constant source of inspiration to me, ever since his supervision of my graduate studies at Stanford

J. Zucker—Thanks to Wilfried Sieg and an anonymous referee for very helpful comments on an earlier draft, and to Mark Armstrong for technical assistance with the typesetting. This research was supported by a grant from the Natural Sciences and Engineering Research Council (Canada).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Notes

  1. 1.

    To avoid confusion, sections in SF’s papers are referred to as Sect. 1, etc., and sections in the present article as §1 and §2, etc.

  2. 2.

    And regrettably never published, but with a far-ranging influence, as we will see in some of the other papers investigated here.

  3. 3.

    This terminology is SF’s.

  4. 4.

    Kleene’s notion of partial recursive functional, given by his schemata S1–S9 [33] or (equivalently for type levels \(\le 2\)) as in [31, p. 326], will feature in every one of the four articles discussed here.

  5. 5.

    Where ‘Sc’ is the successor function on \(\mathbb N\).

  6. 6.

    Gandy to SF, personal communication.

  7. 7.

    The notation and presentation have been changed here to match that in [19], discussed in §3 below.

  8. 8.

    Written ‘\(\pi \)’ in [17]. Notation changed here to match [19]; cf. §3 below.

  9. 9.

    Actually a congruence relation w.r.t. the \(F_k\)’s.

  10. 10.

    Emphasis added. The meaning of this phrase is discussed below.

  11. 11.

    As noted in §1 above.

  12. 12.

    Below I use ‘\(\mathbb N\)’ for ‘\(\omega \)’.

  13. 13.

    This notation ‘ \(\overset{\sim }{\rightarrow }\) ’ for partial functions is not the same as SF’s here, but is used for consistency with his notation in the paper [19] discussed in §3 below.

  14. 14.

    Emphasis added. This gives the essential difference between models 2 and 3.

  15. 15.

    Emphasis added. This gives the essential difference between models 2 and 3.

  16. 16.

    Recall (2.1) the equality relations ‘\(=_{A_i}\)’ on \(\mathcal A\).

  17. 17.

    The notation here has been modified to conform to that in [19], cf. §3 below.

  18. 18.

    That is, model 4 described above.

  19. 19.

    There is an error here, corrected by SF, with an improved presentation, in Sect. 11 of [19] (§3 below). This and a few other corrigenda for the present paper are listed in App. C of that paper.

  20. 20.

    Previously reviewed by me in [60], which lists some (minor) slips in this paper.

  21. 21.

    As in (3.1).

  22. 22.

    My terminology.

  23. 23.

    My terminology.

  24. 24.

    Or more accurately, simultaneously with this lemma.

  25. 25.

    As SF points out, this implies that  \(F\!\upharpoonright \!B:B_{\bar{\sigma }}\times B_{\bar{\imath }}\overset{\sim }{\rightarrow }B_j\), but not conversely.

  26. 26.

    This has already been discussed in [15] (cf. §1 above).

  27. 27.

    Note that this is the stream structure (2.5) without the equalities.

  28. 28.

    As in Platek’s finite type structures [15] (cf. §1 above and Footnote 3).

  29. 29.

    I.e., any linearly ordered subset of \(A_i\) has a l.u.b in \(A_i\).

  30. 30.

    Not given explicitly in [18].

  31. 31.

    As we will see with the recursion scheme shown below.

  32. 32.

    In connection with another recursion scheme, but it is still appropriate here.

  33. 33.

    This supersedes the presentation of this topic in Sect. 12 of [18] (§2 above). See Footnote 19.

  34. 34.

    Unfortunately never published (personal communication by SF).

  35. 35.

    See e.g. [56] and the references therein.

  36. 36.

    Discussed further in §4 below.

  37. 37.

    These issues are discussed in [56, §7],[55, §4.2.14].

  38. 38.

    Emphasis added. Following SF, I shall focus on the real-computability aspect of the various models, rather than their complexity-theoretical or scientific-computational aspects.

  39. 39.

    Emphasis added.

  40. 40.

    See footnote 4.

  41. 41.

    We use “algebra” rather than “structure” to indicate that their signatures contain function (and constant) but not relation symbols.

  42. 42.

    See footnote 4.

References

  1. Bishop, E., Bridges, D.: Constructive Analysis. Springer (1985)

    Google Scholar 

  2. Braverman, M., Cook, S.: Computing over the reals: foundations for scientific computation. Not. Am. Math. Soc. 51, 318–329 (2006)

    MATH  Google Scholar 

  3. Blum, L., Cucker, F., Shub, M., Smale, S.: Complexity and Real Computation. Springer (1998)

    Google Scholar 

  4. Beeson, M.: Foundations of Constructive Mathematics. Springer (1985)

    Google Scholar 

  5. Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill (1967)

    Google Scholar 

  6. Blum, L.: Computability over the reals: where turing meets Newton. Not. Am. Math. Soc. 51, 1024–1034 (2004)

    MATH  Google Scholar 

  7. Blum, L., Shub, M., Smale, S.: On a theory of computation and complexity over the real numbers: NP-completeness, recursive functions and universal machines. Bull. Am. Math. Soc. 21, 1–46 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  8. Bergstra, J.A., Tucker, J.V.: Initial and final algebra semantics for data type specifications: two characterization theorems. SIAM J. Comput. 12, 366–387 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  9. Courant, R., Hilbert, D.: Methods of Mathematical Physics, vol. II. Interscience (1953). Translated and revised from the German edition (1937)

    Google Scholar 

  10. Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer (1998)

    Google Scholar 

  11. Ershov, Y.L.: Computable functions of finite types. Algebra and Logic, 11, 203–242 (1972). Translated from Algebra i Logika, 11, 367–437 (1972)

    Google Scholar 

  12. Ershov, Y.L.: Maximal and everywhere-defined funtionals. Algebra and Logic, 13, 210–225 (1974). Translated from Algebra i Logika, 13, 374–397 (1974)

    Google Scholar 

  13. Feferman, S.: A language and axioms for explicit mathematics. In: Crossley, J.N. (ed.) Algebra and Logic: Papers from the 1974 Summer Research Institute of the Australasian Mathematical Society, vol. 450. Lecture Notes in Mathematics, pp. 87–139. Springer (1975)

    Google Scholar 

  14. Feferman, S.: Generating schemes for partial recursively continuous functionals (Summary). In: Colloque International de Logique, Clermont-Ferrand, 1975, vol. 249. Colloq. Int. du Centre National de la Recherche Scientifique, Paris, pp. 191–198 (1977)

    Google Scholar 

  15. Feferman, S.: Inductive schemata and recursively continuous functionals. In: Gandy, R.O., Hyland, J.M.E. (eds.) Logic Colloquium 76: Proceedings of a Conference held in Oxford in July 1976, pp. 191–198. North Holland (1977)

    Google Scholar 

  16. Feferman, S.: Constructive theories of functions and classes. In: Boffa, M., van Dalen, D., McAloon, K. (eds.) Logic Colloquium ’78: Proceedings of a Colloquium held in Mons, August 1978, pp. 159–224. North Holland (1979)

    Google Scholar 

  17. Feferman, S.: A new approach to abstract data types, I: informal development. Math. Struct. Comput. Sci. 2, 193–229 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  18. Feferman, S.: A new approach to abstract data types, II: computability on adts as ordinary computation. In: Börger, E. et al. (ed.) Computer Science Logic: Proceedings 5th Workshop, Berne, Switzerland, October 1991, vol. 626. Lecture Notes in Computer Science, pp. 79–95. Springer (1992)

    Google Scholar 

  19. Feferman, S.: Computation on abstract data types: the extensional approach, with an application to streams. Ann. Pure Appl. Log. 81, 75–113 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  20. Feferman, S.: About and around computing over the reals. In: Copeland, B.J., Posy, C.J., Shagrir, O. (eds.) Computability: Turing, Gödel, Church, and Beyond, pp. 55–76. MIT Press (2013)

    Google Scholar 

  21. Feferman, S.: Theses for computation and recursion on abstract structure. In: Sommaruga, G., Strahm, T. (eds.) Turing’s Revolution: The Impact of his Ideas about Computability. Birkhäuser/Springer, Basel (2015)

    Google Scholar 

  22. Fenstad, J.E.: On axiomatizing recursion theory. In: Fenstad, J.E., Hinman, P.G. (eds.) Generalized Recursion Theory: Proceedings 1972 Oslo Symposium, pp. 385–404. North Holland (1974)

    Google Scholar 

  23. Friedman, H., Mansfield, R.: Algebraic procedures. Trans. Am. Math. Soc. 332, 297–312 (1992)

    Article  MATH  Google Scholar 

  24. Friedman, H.: Algebraic procedures, generalized Turing algorithms, and elementary recursion theory. In: Gandy, R.O., Yates, C.M.E. (eds.) Logic Colloquium ’69, pp. 361–389. North Holland (1971)

    Google Scholar 

  25. Grzegorczyk, A.: Computable functions. Fundamenta Mathematicae 42, 168–202 (1955)

    Article  MathSciNet  MATH  Google Scholar 

  26. Grzegorczyk, A.: On the defintions of computable real continuous functions. Fundamenta Mathematicae 44, 61–71 (1957)

    Article  MathSciNet  MATH  Google Scholar 

  27. Goguen, J.A., Thatcher, J.W., Wagner, E.G., Wright, J.B.: Initial algebra semantics and continuous algebras. J. Assoc. Comput. Mach. 24, 68–95 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  28. Hadamard, J.: Lectures on Cauchy’s Problem in Linear Partial Differential Equations. Dover (1952). Translated from the French edition (1922)

    Google Scholar 

  29. Hadamard, J.: La Théorie des Équations aux Dérivées Partielles. Éditions Scientifiques (1964)

    Google Scholar 

  30. Hyland, J.M.E.: Recursion Theory on the Conntable Functionals. D.Phil. thesis, Oxford University (1975)

    Google Scholar 

  31. Kleene, S.C.: Introduction to Metamathematics. North Holland (1952)

    Google Scholar 

  32. 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 (1959)

    Google Scholar 

  33. Kleene, S.C.: Recursive functionals and quantifiers of finite types i. Trans. Am. Math. Soc. 91, 1–52 (1959)

    MathSciNet  MATH  Google Scholar 

  34. Kechris, A.S., Moschovakis, Y.N.: Recursion in higher types. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 681–737. North Holland (1977)

    Google Scholar 

  35. Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite type. In: Heyting, A. (ed.) Constructivity in Mathematics: Proceedings of the Colloquium held at Amsterdam, 1957, pp. 101–128. North Holland (1959)

    Google Scholar 

  36. Lacombe, D.: Extension de la notion de fonction récursive aux fonctions d’une ou plusieurs variables réelles, I, II, III. C.R. Acad. Sci. Paris (1955), 240, 2470–2480, 241, 13–14, 151–153

    Google Scholar 

  37. Moschovakis, Y.N.: Abstract first order computability I. Trans. Am. Math. Soc. 138, 427–464 (1969)

    MathSciNet  MATH  Google Scholar 

  38. Moschovakis, Y.N.: Axioms for computation theories — first draft. In: Gandy, R.O., Yates, C.E.M. (eds.) Logic Colloquium ’69: Proceedings Summer School Colloquium in Mathematical Logic, Manchester, August 1969, pp. 199–255. North Holland (1971)

    Google Scholar 

  39. Moschovakis, Y.N.: Elementary Induction on Abstract Structures. North Holland (1974)

    Google Scholar 

  40. Moschovakis, Y.N.: On the basic notions in the theory of induction. In: Proceedings of the 5th International Congress in Logic, Methodology and Philosophy of Science, London, Ontario, 1975, pp. 207–236 (1976)

    Google Scholar 

  41. Moschovakis, Y.N.: Abstract recursion as a foundation for the theory of recursive algorithms. In: Richter, M.M. et al. (ed.) Computation and Proof Theory: Proceedings Logic Colloquium Aachen 1983, Part II, vol. 1104. Lecture Notes in Mathematics, pp. 289–364. Springer (1984)

    Google Scholar 

  42. Moschovakis, Y.N.: The formal language of recursion. J. Symb. Log. 54, 1216–1252 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  43. Mitchell, J.C., Plotkin, G.D.: Abstract types have extensional type. ACM Trans. Progr. Lang. Syst. 10, 470–502 (1985)

    Article  Google Scholar 

  44. Myhill, J., Shepherdson, J.: Effective operations on partial recursive functions. Zeitschr. Msth. Logik u. Grundlagen. Math. 1, 310–317 (1955)

    Article  MathSciNet  MATH  Google Scholar 

  45. Moldestat, J., Stoltenberg-Hansen, V., Tucker, J.V.: Finite algorithmic procedures and computation theories. Mathematica Scandinavica 46, 77–94 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  46. Moldestat, J., Stoltenberg-Hansen, V., Tucker, J.V.: Finite algorithmic procedures and inductive definability. Mathematica Scandinavica 46, 62–76 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  47. Pour-El, M.B., Richards, J.I.: Computability in Analysis and Physics. Springer (1989)

    Google Scholar 

  48. Platek, R.A.: Foundations of Recursion Theory. Ph.D. thesis, Department of Mathematics, Stanford University (1966)

    Google Scholar 

  49. Sazonov, V.Y.: Degrees of parallelism in computation. In: Mazurkiewicz, A. (ed.) Proceedings of the 5th Symposium Mathematical Foundations of Computer Science (MFCS’76), Gdansk, September 1976

    Google Scholar 

  50. Smullyan, R.M.: Theory of Formal Systems, vol. 47. Annals of Mathematical Studies. Princeton University Press (1961)

    Google Scholar 

  51. Strong Jr., H.R.: Translating recursion equations into flowcharts. J. Comput. Syst. Sci. 5, 254–285 (1971)

    Article  MATH  Google Scholar 

  52. Tucker, J.V., Zucker, J.I.: Program Correctness over Abstract Data Types, with Error-State Semantics, vol. 6. CWI Monographs. North Holland (1988)

    Google Scholar 

  53. Tucker, J.V., Zucker, J.I.: Computable functions and semicomputable sets on many-sorted algebras. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 5, pp. 317–523. Oxford University Press (2000)

    Google Scholar 

  54. Tucker, J.V., Zucker, J.I.: Abstract versus concrete computation on metric partial algebras. ACM Trans. Comput. Log. 5, 611–668 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  55. Tucker, J.V., Zucker, J.I.: Continuity of operators on continuous and discrete time streams. Theoret. Comput. Sci. 412, 3378–3403 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  56. Tucker, J.V., Zucker, J.I.: Generalizing computability to abstract algebras. In: Sommaruga, G., Strahm, T. (eds.) Turing’s Revolution: The Impact of his Ideas about Computability. Birkhauser/Springer, Basel (2015)

    Google Scholar 

  57. Weihrauch, K.: Computable Analysis: An Introduction. Springer (2000)

    Google Scholar 

  58. Jian, Xu, Zucker, Jeffery: First and second order recursion on abstract data types. Fundamenta Informaticae 21, 1–43 (2004)

    Google Scholar 

  59. Ye, Feng: Toward a constructive theory of unbounded linear operators. J. Symb. Log. 65, 357–370 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  60. Zucker, J.I.: Review of [18]. Bull. Symb. Log. 8, 538–542 (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing and Software, McMaster University, Hamilton, ON, L8S 4K1, Canada

    Jeffery Zucker

Authors
  1. Jeffery Zucker
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jeffery Zucker .

Editor information

Editors and Affiliations

  1. Institut für Informatik, Universität Bern, Bern, Switzerland

    Gerhard Jäger

  2. Department of Philosophy, Carnegie Mellon University Dept. Philosophy, Pittsburgh, Pennsylvania, USA

    Wilfried Sieg

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Zucker, J. (2017). Feferman on Computability. In: Jäger, G., Sieg, W. (eds) Feferman on Foundations. Outstanding Contributions to Logic, vol 13. Springer, Cham. https://doi.org/10.1007/978-3-319-63334-3_2

Download citation

Publish with us

Policies and ethics

Search

Navigation