Abstract
We aim at providing a philosophical analysis of the notion of “proof by Church’s Thesis”, which is – in a nutshell – the conceptual device that permits to rely on informal methods when working in Computability Theory. This notion allows, in most cases, to not specify the background model of computation in which a given algorithm – or a construction – is framed. In pursuing such analysis, we carefully reconstruct the development of this notion (from Post to Rogers, to the present days), and we focus on some classical constructions of the field, such as the construction of a simple set. Then, we make use of this focus in order to support the following encompassing claim (which opposes to a somehow commonly received view): the informal side of Computability, consisting of the large class of methods typically employed in the proofs of the field, is not fully reducible to its formal counterpart.
The author was partially supported by the Austrian Science Fund FWF through project P 27527.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
A classical introduction to CTT can be found in Kleene (1952). See also Church (1936), Turing (1936, 1948), Post (1936), and Gödel (1946). Soare (1987b) contains, in its first part, an accurate reconstruction of the role of Turing’s work in the acceptance of the thesis. For recent philosophical work concerning CTT, the reader is referred, for instance, to Olszewski et al. (2006).
- 2.
The standard interpretation is that CTT is indeed a thesis, or, in Post’s words, “a working hyphotesis” (Post 1936). That is to say, something that cannot be subject of a mathematical proof. Yet, it has been argued that CTT has not necessarily an hypothetical status, but rather that it can be susceptible of a rigorous mathematical proof, or even that such a proof is already contained in Turing (1936) (for this line of thought see, e.g., Mendelson (1990), Gandy (1988), Sieg (1994), and the discussion contained in Shapiro (2006)). Responses to this latter position can be found in Folina (1998) and Black (2000).
- 3.
- 4.
For instance, the following is the first proof-theoretic reference to CTT in Rogers (1967):
Theorem 1
There are exactly ℵ 0 partial recursive functions, and there are exactly ℵ 0 recursive functions.
Proof
All constants functions are recursive, by Church’s Thesis. Hence there are at least ℵ 0 recursive functions. The Gödel numbering shows that there are at most ℵ 0 partial recursive functions.
- 5.
To be fair, Post mainly speaks of computably enumerable sets, there introduced for the first time. But since, by definition, a set is computably enumerable if it is the range of a computable function, then one can trivially translate Post’s formulations in instances of our prototype.
- 6.
It is worth noticing that the Leibnizian ideal is by no means archeological. Quite to the contrary. Hacking reports Voevodsky’s opinion that “in a few years, journal will accept only articles accompanied by their machine-verifiable equivalents”. More generally – and less radically – research on proof-assistants can be (partially) motivated as a way of improving automatic verification of proofs.
- 7.
For an accurate reconstruction of Post’s thought see De Mol (2006)
- 8.
From now on, in describing the practical side of CTT, we will mostly refer to textbooks. This is a natural choice. Since, as already said, there are no philosophical studies concerning the practice of Computability, the most immediate source of observations regarding how such practice has to be intended comes from the kind of expository remarks that abound in books such as Rogers’.
- 9.
The interested reader can consult Mancosu (2008) for an anthology of papers in Philosophy of Mathematical Practice.
- 10.
\(\mathbb {I}\) does clearly correspond to a pre-theoretic object whose formalization would be far from trivial. For instance, there could be a worry concerning a sort of Berry-like paradox, inasmuch we admit a too relaxed notion on what counts as an informal description for an algorithm. Nonetheless, we can suppose to deal with sufficiently clear descriptions. This is because, although border-cases cannot arguably be expunged, we are more interested, as we will see, in a somewhat global tendency.
- 11.
All of this is of course related to the philosophical problem of determining if one can possibly formulate a definition for algorithms that would be correct in the sense of Shore: “Find, and argue conclusively for, a formal definition of algorithm and the appropriate analog of the Church-Turing thesis. Here we want to capture the intuitive notion that, for example, two particular programs in perhaps different languages express the same algorithm, while other ones that compute the same function represent different algorithms for the function. Thus we want a definition that will up to some precise equivalence relation capture the notion that two algorithms are the same as opposed to just computing the same function”(Buss et al. 2001). See also Dean (2007) for a rich discussion on whether algorithms can be fairly regarded as abstract mathematical objects.
- 12.
Indeed, Blass et al. (2009) argue that “one cannot give a precise equivalence relation capturing the intuitive notion of ‘the same algorithm.”’
- 13.
- 14.
Some equivalence between classical models of computation can be found in Odifreddi (1989).
- 15.
For a classical defense of structuralism in philosophy of mathematics, the reader is referred to Resnik (1997).
- 16.
References
Awodey, S. 2014. Structuralism, invariance, and univalence. Philosophia Mathematica 22(1): 1–11.
Black, R. 2000. Proving Church’s thesis. Philosophia Mathematica 8(3): 244–258.
Blass, A., N. Dershowitz, and Y. Gurevich. 2009. When are two algorithms the same? Bulletin of Symbolic Logic 15(02): 145–168.
Burgess, J.P. 2015. Rigor and structure. Oxford: Oxford University Press.
Buss, S.R., A.S. Kechris, A. Pillay, and R.A. Shore. 2001. The prospects for mathematical logic in the twenty-first century. Bulletin of Symbolic Logic 7(02): 169–196.
Carter, J. 2008. Structuralism as a philosophy of mathematical practice. Synthese 163(2): 119–131.
Church, A. 1936. An unsolvable problem of elementary number theory. American Journal of Mathematics 58(2): 345–363.
Davis, M. 2006. Why there is no such discipline as hypercomputation. Applied Mathematics and Computation 178(1): 4–7.
De Mol, L. 2006. Closing the circle: An analysis of Emil Post’s early work. Bulletin of Symbolic Logic 12(02): 267–289.
Dean, W.H. 2007. What algorithms could not be. PhD thesis, Rutgers University-New Brunswick.
Descartes, R. 1628. Rules for the direction of the mind. In Selections. Trans. R.M. Eaton. New York: Charles Scribner’s Sons, 1927.
Epstein, R.L., and W. Carnielli. 1989. Computability: Computable functions, logic, and the foundations of mathematics. Pacific Grove: Wadsworth & Brooks/Cole.
Fallis, D. 2003. Intentional gaps in mathematical proofs. Synthese 134(1): 45–69.
Folina, J. (1998). Church’s thesis: Prelude to a proof. Philosophia Mathematica 6(3): 302–323.
Gandy, R. 1988. The confluence of ideas in 1936. In The Universal Turing machine: A half-century survey, ed. R. Herken, 55–111. Wien/New York: Springer.
Gödel, K. 1946. Remarks before the Princeton bicentennial conference on problems in mathematics. In Kurt Gödel: Collected works, ed. S. Feferman, J. Dawson, and S. Kleene, vol. II, pp. 150–153. Oxford: Oxford University Press.
Gurevich, Y. 2000. Sequential abstract-state machines capture sequential algorithms. ACM Transactions on Computational Logic (TOCL) 1(1): 77–111.
Hacking, I. 2014. Why is there philosophy of mathematics at all? Cambridge: Cambridge University Press.
Hilbert, D. 1899. Grundlagen der geometrie. In Festschrift zur Feier der Enthüllung des Gauss-Weber-Denkmals in Göttingen, 1–92. Leipzig: Teubner.
Kleene, S.C. 1952. Introduction to metamathematics. Amsterdam: North Holland.
Lakatos, I. 1976. Proofs and refutations: The logic of mathematical discovery. Cambridge: Cambridge University Press.
Mancosu, P. 2008. The philosophy of mathematical practice. Oxford: Oxford University Press.
McLarty, C. 2008. What structuralism achieves. In Mancosu (2008).
Mendelson, E. 1990. Second thoughts about Church’s thesis and mathematical proofs. The Journal of Philosophy 87(5): 225–233.
Odifreddi, P. 1989. Classical recursion theory, vol. I. Amsterdam: North Holland.
Olszewski, A., J. Wolenski, and R. Janusz. 2006. Church’s thesis after 70 years. Frankfurt/New Brunswick: Ontos Verlag.
Post, E.L. 1936. Finite combinatory processes–formulation. The Journal of Symbolic Logic 1(03): 103–105.
Post, E.L. 1944. Recursively enumerable sets of positive integers and their decision problems. Bulletin of the American Mathematical Society 50(5): 284–316.
Rav, Y. 1999. Why do we prove theorems? Philosophia Mathematica 7(1): 5–41.
Resnik, M.D. 1997. Mathematics as a science of patterns. Oxford: Oxford University Press.
Rogers, H., Jr. 1967. Theory of recursive functions and effective computability. New York: McGraw-Hill.
Shapiro, S. 2006. Computability, proof, and open-texture. In Olszewski et al. (2006), 420–455.
Shapiro, S. 2010. Mathematical structuralism. Internet Encyclopedia of Philosophy. https://www.iep.utm.edu/m-struct/. 25 June 2018.
Sieg, W. 1994. Mechanical procedures and mathematical experience. In Mathematics and mind, ed. A. George, 71–117. Oxford: Oxford University Press.
Soare, R.I. 1987a. Recursively enumerable sets and degrees. Perspectives in mathematical logic, omega series. Heidelberg: Springer.
Soare, R.I. 1987b. Interactive computing and relativized computability, In Computability: Turing, Gödel, Church, and beyond, ed. B.J. Copeland, C.J. Posy, and O. Shagrir, 203–260. Cambdrige: MIT Press.
Turing, A.M. 1936. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London Mathematical Society 2(1): 230–265.
Turing, A.M. 1948. Intelligent machinery. In Collected works of A.M. Turing: Mechanical intelligence, ed. D.C. Ince, 107–127. Amsterdam: North-Holland
Welch, P.D. 2007. Turing unbound: Transfinite computation. In Computation and logic in the real world, ed. B. Löwe, B. Cooper, and A. Sorbi, 768–780. Berlin: Springer.
Wittgenstein, L. 1980. Remarks on the philosophy of psychology. Oxford: Blackwell.
Acknowledgements
A preliminary version of this paper appeared as a chapter of my PhD thesis. I would like to thank my supervisors, Gabriele Lolli and Andrea Sorbi, for their guidance and support. I have presented this work at several conferences. In particular, I am grateful to the participants of APMP 2014, in Paris, and of FilMat 2016, in Chieti, for their comments. Finally, Richard Epstein’s remarks were fundamental in rethinking the organization of the present material.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
Cite this chapter
Mauro, L.S. (2018). Church-Turing Thesis, in Practice. In: Piazza, M., Pulcini, G. (eds) Truth, Existence and Explanation. Boston Studies in the Philosophy and History of Science, vol 334. Springer, Cham. https://doi.org/10.1007/978-3-319-93342-9_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-93342-9_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-93341-2
Online ISBN: 978-3-319-93342-9
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)