Hostname: page-component-78c5997874-lj6df Total loading time: 0 Render date: 2024-11-05T05:45:54.927Z Has data issue: false hasContentIssue false
  • English
  • Français

A Natural Axiomatization of Computability and Proof of Church's Thesis

Published online by Cambridge University Press:  15 January 2014

Nachum Dershowitz  and
Yuri Gurevich
Nachum Dershowitz
Affiliation:
Microsoft Research, Redmond, WA 98052, USAand School of Computer Science, Tel Aviv University, Ramat Aviv 69978, Israel, E-mail: [email protected]: www.cs.tau.ac.il/~nachum
Yuri Gurevich
Affiliation:
Microsoft Research, Redmond, WA 98052, USAE-mail: [email protected]: research.microsoft.com/~gurevich
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Church's Thesis asserts that the only numeric functions that can be calculated by effective means are the recursive ones, which are the same, extensionally, as the Turing-computable numeric functions. The Abstract State Machine Theorem states that every classical algorithm is behaviorally equivalent to an abstract state machine. This theorem presupposes three natural postulates about algorithmic computation. Here, we show that augmenting those postulates with an additional requirement regarding basic operations gives a natural axiomatization of computability and a proof of Church's Thesis, as Gödel and others suggested may be possible. In a similar way, but with a different set of basic operations, one can prove Turing's Thesis, characterizing the effective string functions, and—in particular—the effectively-computable functions on string representations of numbers.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 14 , Issue 3 , September 2008 , pp. 299 - 350
Copyright
Copyright © Association for Symbolic Logic 2008

References

REFERENCES

[1] Alliance for Telecommunications Industry Solutions, Committee T1A1 Performance and Sinal Processing, ATIS Telecom Glossary 2000, American National Standards Institute Document ANS T1.523-2001, approved 28 February 2001. Latest version available at http://www.atis.org/glossary/definition.aspx?id=7687 (viewed Apr. 23, 2008).Google Scholar
[2] Barendregt, Henk, The impact of the lambda calculus in logic and computer science, this Bulletin, vol. 3 (1997), no. 2, pp. 181–215, available at http://www.math.ucla.edu/~asl/bsl/0302/0302-003.ps (viewed Apr. 21, 2008).Google Scholar
[3] Barzdin, Janis M., Ob odnom klasse mashin Tjuringa (mashiny Minskogo)[Onaclass of Turing machines (Minsky machines)], Algebra i Logika [Algebra and Logic], vol. 1 (1963), no. 6, pp. 42–51, in Russian.Google Scholar
[4] Befmann, Heinrich, Beitrage zur Algebra der Logik, insbesondere zum Entscheidungsproblem, Mathematische Annalen, vol. 86 (1922), pp. 163–229, in German.CrossRefGoogle Scholar
[5] Bergstra, Jan A. and Tucker, Jofn V., Algebraic specifications of computable and semi-computable datastructures, Theoretical Computer Science, vol. 50 (1987), no. 2, pp. 137–181.CrossRefGoogle Scholar
[6] Black, Robert, Proving Church's thesis, Philosophia Mathematica, vol. 8 (2000), pp. 244–258.Google Scholar
[7] Blass, Andreas, Dershowitz, Nachum, and Gurevich, Yuri, When are two algorithms the same?, Technical Report MSR-TR-2008-20, Microsoft Research, Redmond, WA, February 2008, available at http://research.microsoft.com/~gurevich/Opera/192.pdf (viewed Apr. 30, 2008).Google Scholar
[8] Blass, Andreas and Gurevich, Yuri, Algorithms vs. machines, Bulletin of the European Association for Theoretical Computer Science, (2002), no. 77, pp. 96–118, reprinted in Current Trends in Theoretical Computer Science: The Challenge ofthe New Century, vol. 2, Formal Models and Semantics (G. Paun, G. Rozenberg, and A. Salomaa, editors), World Scientific Publishing Company, 2004, pp. 215–236. Available at http://research.microsoft.com/~gurevich/Opera/158.pdf (viewed Nov. 28, 2007).Google Scholar
[9] Blass, Andreas, Abstract state machines capture parallel algorithms, ACM Transactions on Computational Logic, vol. 4 (2003), no. 4, pp. 578–651, available at http://research.microsoft.com/~gurevich/Opera/157-1.pdf (viewed Nov. 28, 2007). See also: Abstract state machines capture parallel algorithms: Correction and extension, ACM Transactions on Computational Logic , vol. 9, no. 3, in press, available at http://tocl.acm.org/accepted/314gurevich.pdf (viewed Nov. 28, 2007).CrossRefGoogle Scholar
[10] Blass, Andreas, Algorithms: A quest for absolute definitions, Church's Thesis after 70 years (Olszewski, A., Wolenski, J., and Janusz, R., editors), Ontos Verlag, 2006, pp. 24–57. Also in Bulletin of the European Association for Theoretical Computer Science, (2003), no. 81, pp. 195–225, and in Current trends in theoretical computer science, World Scientific, 2004, pp. 283–311, available at http://research.microsoft.com/~gurevich/Opera/164.pdf (viewed Nov. 28, 2007).CrossRefGoogle Scholar
[11] Blass, Andreas, Ordinary interactive small-step algorithms, I, ACM Transactions on Computational Logic, vol. 7 (2006), no. 2, pp. 363–419, available at http://tocl.acm.org/accepted/blass04.ps (viewed Apr. 23, 2008).Google Scholar
[12] Blass, Andreas, Ordinary interactive small-step algorithms, II, ACM Transactions on Computational Logic, vol. 8 (2007), no. 3, available at http://tocl.acm.org/accepted/blass2.ps (viewed Apr. 23, 2008).Google Scholar
[13] Blass, Andreas, Ordinary interactive small-step algorithms, III, ACM Transactions on Computational Logic, vol. 8 (2007), no. 3, available at http://tocl.acm.org/accepted/250blass.pdf (viewed Apr. 23, 2008).Google Scholar
[14] Blass, Andreas, Why sets?, Pillars of computer science: Essays dedicated to Boris (Boaz) Trakhtenbrot on the occasion of his 85th birthday (Avron, A., Dershowitz, N., and Rabinovich, A., editors), Lecture Notes in Computer Science, vol. 4800, Springer-Verlag, Berlin, 2008, pp. 179–198, available at http://research.microsoft.com/~gurevich/Opera/172.pdf (viewed Mar. 8, 2008).Google Scholar
[15] Blass, Andreas, Gurevich, Yuri, Rosenzweig, Dean, and Rossman, Benjamin, Interactive small-step algorithms I: Axiomatization, Logical Methods in Computer Science, vol. 3 (2007), no. 4, available at http://research.microsoft.com/~gurevich/Opera/176.pdf (viewed Dec. 16, 2007).Google Scholar
[16] Blass, Andreas, Interactive small-step algorithms II. Abstract state machines and the characterization theorem, Logical Methods in Computer Science, vol. 3 (2007), no. 4, available at http://research.microsoft.com/~gurevich/Opera/182.pdf (viewed Dec. 16, 2007).Google Scholar
[17] Boker, Udi and Dershowitz, Nachum, Abstract effective models, New developments in computational models: Proceedings of the first international workshop on Developments in Computational Models (DCM 2005) (Lisbon, Portugal, July 2005) (Fernández, M. and Mackie, I., editors), vol. 135, Electronic Notes in Theoretical Computer Science, no. 3, February 2006, pp. 15–23, available at http://www.cs.tau.ac.il/~nachum/papers/AbstractEffectiveModels.pdf (viewed Nov. 28, 2007).Google Scholar
[18] Boker, Udi, Comparing computational power, Logic Journal of the IGPL, vol. 14 (2006), no. 5, pp. 633–648, available at http://www.cs.tau.ac.il/~nachum/papers/ComparingComputationalPower.pdf (viewed Nov. 28, 2007).CrossRefGoogle Scholar
[19] Boker, Udi, The Church-Turing Thesis over arbitrary domains, Pillars of computer science: Essays dedicated to Boris (Boaz) Trakhtenbrot on the occasion of his 85th birthday (Avron, A., Dershowitz, N., and Rabinovich, A., editors), Lecture Notes in Computer Science, vol. 4800, Springer-Verlag, Berlin, 2008, pp. 199–229, available at http://www.cs.tau.ac.nachum/papers/ArbitraryDomains.pdf (viewed Nov. 28, 2007).CrossRefGoogle Scholar
[20] Börger, Egon, The origins and the development of the ASM method for high level system design and analysis, Journal ofUniversal Computer Science, vol. 8 (2002), no. 1, pp. 2–74.Google Scholar
[21] Buss, Samuel R., Kechris, Alexander A., Pillay, Anand, and Shore, Richard A., The prospects for mathematical logic in the twenty-first century, this Bulletin, vol. 7 (2001), no. 2, pp. 169–196, available at http://www.math.ucla.edu/~asl/bsl/0702/0702-001.ps (viewed Apr. 21, 2008).Google Scholar
[22] Church, Alonzo, Anoteon the Entscheidungsproblem, The Journal of Symbolic Logic, vol. 1 (1936), no. 1, pp. 40–41; Corrigendum, The Journal of Symbolic Logic , vol. 1 (1936), no. 3, pp. 101–102. Reprinted in [27], pp. 110–115.CrossRefGoogle Scholar
[23] Church, Alonzo, An unsolvable problem of elementary number theory, American Journal of Mathematics, vol. 58 (1936), pp. 345–363, reprinted in [27], pp. 89–107. Available at doi: 10.2307/2371045.Google Scholar
[24] Church, Alonzo, Review of Alan M. Turing, On computable numbers, with an application to the Entscheidungsproblem (Proceedings of the London Mathematical Society, vol. 2 (1936), no. 42, pp. 230–265), The Journal of Symbolic Logic , vol. 2 (1937), pp. 42–43.Google Scholar
[25] Church, Alonzo, Review of Emil Post, Finite combinatory processes, Formulation I (The Journal of Symbolic Logic, vol. 1 (1936), pp. 103–105), The Journal of Symbolic Logic , vol. 2 (1937), p. 43.Google Scholar
[26] Copeland, B. Jack, The Church-Turing Thesis, Stanford encyclopedia of philosophy (Zalta, E., editor), 1996, available at http://plato.stanford.edu/entries/church-turing (viewed Nov. 28, 2007).Google Scholar
[27] Davis, Martin (editor), The undecidable: Basic papers on undecidable propositions, unsolvable problems and computable functions, Raven Press, Hewlett, NY, 1965, reprinted by Dover Publications, Mineola, NY, 2004.Google Scholar
[28] Davis, Martin, Why Gödel didn't have Church's thesis, Information and Control, vol. 54 1982), pp. 3–24.Google Scholar
[29] Davis, Martin D., Sigal, Ron, and Weyuker, Elaine J., Computability, complexity, and languages: Fundamentals of theoretical computer science, 2nd ed., Academic Press, San Diego, CA, 1994.Google Scholar
[30] Dawar, Anuj, Richerby, David, and Rossman, Benjamin, Choiceless polynomial time, counting and the Cai-Fürer-Immerman graphs, Annals of Pure and Applied Logic, vol. 152 (2008), pp. 31–50, available at http://www.mit.edu/~brossman/CPT-CFI.pdf (viewed Apr. 30, 2008).CrossRefGoogle Scholar
[31] Folina, Janet, Church's thesis: Prelude to a proof, Philosophia Mathematica, vol. 6 (1998), no. 3, pp. 302–323.CrossRefGoogle Scholar
[32] Fredkin, Edward F. and Toffoli, Tommaso, Conservative logic, International Journal of Theoretical Physics, vol. 21 (1982), no. 3/4, pp. 219–253.Google Scholar
[33] Friedman, Harvey M., Mathematical logic in the 20th and 21st centuries, FOM-Foundations of Mathematics mailing list, April 27 2000, available at http://cs.nyu.edu/pipermail/fom/2000-April/003913.html (viewed Mar. 27, 2008).Google Scholar
[34] Fröhlich, Albrecht and Shepherdson, John C., Effective procedures in field theory, Philosophical transactions of the Royal Society of London, Series A, vol. 248 (1956), pp. 407–432.Google Scholar
[35] Gandy, Robin O., Church's Thesis and principles for mechanisms, The Kleene symposium (Barwise, J., Kaplan, D., Keisler, H. J., Suppes, P., and Troelstra, A. S., editors), Studies in Logic and the Foundations of Mathematics, vol. 101, North-Holland, Amsterdam, 1980, pp. 123–148.Google Scholar
[36] Gandy, Robin O., The confluence of ideas in 1936, The universal Turing machine: A half-century survey (Herken, R., editor), Oxford University Press, New York, 1988, pp. 55–111.Google Scholar
[37] Glausch, Andreas and Reisig, Wolfgang, An ASM-characterization of a class ofdistributed algorithms, Proceedings of the Dagstuhl seminar on rigorous methods for software construction and analysis (Abrial, J.-R. and Glässer, U., editors), May 2006, available at http://www2.informatik.hu-berlin.de/top/download/publications/GlauschR2007_dagstuhl.pdf (viewed Mar. 26, 2008). Longer version: Distributed abstract state machines and their expressive power, Informatik-Berichte 196, Humboldt-Universität zu Berlin, Jan. 2006, available at http://www2.informatik.hu-berlin.de/top/download/publications/GlauschR2006_hub_trl96.pdf (viewed Mar. 26, 2008).Google Scholar
[38] Gödel, Kurt, On undecidable propositions of formal mathematical systems, in [27], pp. 41–73, based on lecture notes from 1934.Google Scholar
[39] Gödel, Kurt Gödel *193?: [Undecidable diophantine propositions], Unpublished essays and lectures, Kurt Gödel: Collected works (Feferman, S., Dawson, J. W. Jr., Goldfarb, W., Parsons, C., and Solovay, R. N., editors), vol. III, Oxford University Press, Oxford, 1995, pp. 164–174.Google Scholar
[40] Gold, E. Mark, Limiting recursion, The Journal of Symbolic Logic, vol. 30 (1965), no. 1, pp. 28–48.Google Scholar
[41] Gurevich, Yuri, Evolving algebras 1993: Lipari guide, Specification and validation methods (Börger, E., editor), Oxford University Press, Oxford, 1995, available at http://research.microsoft.com/~gurevich/Opera/103.pdf (viewed Nov. 28, 2007), pp. 9–36.Google Scholar
[42] Gurevich, Yuri, Sequential abstract state machines capture sequential algorithms, ACM Transactions on Computational Logic, vol. 1 (2000), no. 1, pp. 77–111, available at http://tocl.acm.org/accepted/gurevich.ps (viewed Apr. 23, 2008).Google Scholar
[43] Gurevich, Yuri and Huggins, James C., The semantics of the C programming language, Proceedings of the sixth workshop on Computer Science Logic (CSL '92) (Berlin), Lecture Notes in Computer Science, vol. 702, Springer-Verlag, 1993, pp. 274–308, 334–336, available at http://research.microsoft.com/~gurevich/Opera/98.pdf (viewed Mar. 13, 2008).Google Scholar
[44] Hilbert, David, Mathematische Probleme: Vortrag, gehalten auf dem internationalen Mathematiker-Kongreß zu Paris 1900, in German, available at http://www.mathematik.uni-bielefeld.de/~kersten/hilbert/rede.html (viewed Nov. 28, 2007).Google Scholar
[45] Hilbert, David and Ackermann, Wilfelm, Grundzüge der theoretischen Logik, Springer-Verlag, Berlin, 1928, in German. English version of the second (1938) edition: Principles oftheoretical logic (R. E. Luce, translator and editor), AMS Chelsea Publishing, New York, 1950.Google Scholar
[46] Kalmár, László, An argument against the plausibility of Church's thesis, Constructivity in mathematics (Heyting, A., editor), North-Holland, Amsterdam, 1959, pp. 201–205.Google Scholar
[47] Kangshen, Shen, Crossley, John N., and Lun, Anthony W. C., The nine chapters on the mathematical art: Companion and commentary, Oxford University Press, Oxford, 1999.Google Scholar
[48] Kleene, Stephen C., Recursive predicates and quantifiers, Transactions of the American Mathematical Society, vol. 53 (1943), no. 1, pp. 41–73, reprinted in [27], pp. 255–287.Google Scholar
[49] Kleene, Stephen C., Introduction to metamathematics, D. Van Nostrand, New York, 1952.Google Scholar
[50] Kleene, Stephen C., Mathematical logic, John Wiley, New York, 1967, reprinted by Dover, Mineola, NY, 2002.Google Scholar
[51] Kleene, Stephen C., Origins of recursive function theory, IEEE Annals of the History of Computing, vol. 3 (1981), no. 1, pp. 52–67, preliminary version in Proceedings of the 20th annual IEEE symposium on Foundations of Computer Science (FOCS), San Juan, PR, Oct. 1979, pp. 371–382.Google Scholar
[52] Kleene, Stephen C., Reflections on Church's thesis, Notre Dame Journal of Formal Logic, vol. 28 (1987), no. 4, pp. 490–498.Google Scholar
[53] Kleene, Stephen C., Turing's analysis of computability, and major applications of it, The universal Turing machine: A half-century survey (Herken, R., editor), Oxford University Press, New York, 1988, pp. 17–54.Google Scholar
[54] Knuth, Donald E., Algorithm and program; information and data, Communications of the ACM, vol. 9 (1966), no. 9, p. 654.Google Scholar
[55] Knuth, Donald E., Fundamental algorithms, The art of computer programming, vol. 1, Addison-Wesley, Reading, MA, 3rd ed., 1997.Google Scholar
[56] Kolmogorov, Andreĭ N., O ponyatii algoritma [On the concept of algorithm], Uspekhi Matematicheskikh Nauk [Russian Mathematical Surveys], vol. 8 (1953), no. 4, pp. 175–176, in Russian. English version in [111, pp. 18–19].Google Scholar
[57] Kolmogorov, Andreĭ N. and Uspensky, Vladimir A., K opredeleniu algoritma, Uspekhi Matematicheskikh Nauk [Russian Mathematical Surveys], vol. 13 (1958), no. 4, pp. 3–28, in Russian. English version: On the definition of an algorithm, American Mathematical Society Translations, Series II, vol. 29, 1963, pp. 217–245.Google Scholar
[58] Kreisel, Georg, Mathematical logic, Lectures in modern mathematics III (Saaty, T. L., editor), Wiley and Sons, New York, 1965, pp. 95–195.Google Scholar
[59] Kreisel, Georg, Mathematical logic: What has it done for the philosophy of mathematics, Bertrand Russell: Philosopher of the century (Schoenman, R., editor), Allen & Unwin, London, 1967, pp. 201–272.Google Scholar
[60] Krlpke, Saul, Elementary recursion theory and its applications to formal systems, unpublished preliminary draft, 1996.Google Scholar
[61] Krlpke, Saul, From the Church-Turing thesis to the first-order algorithm theorem, Proceedings of the 15th annual IEEE symposium on Logic in Computer Science, Santa Barbara, CA, June 2000, p. 177. Recorded lecture at http://www.vanleer.org.il/eng/videoShow.asp?id=317 (viewed Mar. 28, 2008).Google Scholar
[62] Lambert, William M. Jr., A notion of effectiveness in arbitrary structures, The Journal of Symbolic Logic, vol. 33 (1968), no. 4, pp. 577–602.Google Scholar
[63] Lucas, John R., Review of Judson C. Webb, Mechanism, mentalism and metamathematics: An essay on finitism (D. Reidel, Dordrecht, 1980), The British Journal for the Philosophy of Science, vol. 33 (1982), no. 4, pp. 441–444.Google Scholar
[64] Mal'cev, Anatoliiĭ., Konstruktivnyye algyebry. 1, Uspekhi Matematicheskikh Nauk, vol. 16 (1961), no. 3, pp. 3–60. English version: Constructive algebras, I, The meta-mathematics of algebraic systems (K. A. Hirsch, translator), Russian Mathematical Surveys, vol. 16 (1961), no. 3, pp. 77–129. Also in: The metamathematics of algebraic systems. Collected papers 1936–1967, B. F. Wells, III, editor, North-Holland, Amsterdam, 1971, pp. 148–212.Google Scholar
[65] Manna, Zohar and Shamir, Adi, The optimal approach to recursive programs, Communications of the ACM, vol. 20 (1977), no. 11, pp. 824–831.Google Scholar
[66] Markov, Andreĭ A., Teoriia algorifmov, Works of the Mathematics Institute Im. V. A. Steklov, vol. 42, 1954, in Russian. English version: Theory of algorithms (J. J. Schorr-Kon, translator), American Mathematical Society Translations, Series 2, vol. 15, pp. 1–14, and Israel Program for Scientific Translations, Jerusalem, 1961.Google Scholar
[67] Matijasevic̆, Yuri V., Enumerable sets are Diophantine, Doklady Akademiia Nauk SSSR, vol. 191 (1970), no. 2, pp. 279–282, in Russian. English version: Soviet Mathematics, vol. 11 (1970), no. 2, pp. 354–357.Google Scholar
[68] Menabrea, Luigi Federico, Notions sur la machine analytique de M Charles Babbage, Bibliothèque Universelle de Geneve n.s., vol. 41 (1842), pp. 352–376, in French. Also in: Charles Babbage, The works of Charles Babbage (M. Campbell-Kelly, editor), vol. 3, The difference engine and table making, NYU Press, New York, 1989, pp. 62–82. English version: Sketch ofthe Analytical Engine invented by Charles Babbage (with notes upon the memoir by the translator A. A. L. [Ada Augusta, Countess of Lovelace]), Scientific Memoirs (R. Taylor, editor), vol. 3, 1843, pp. 666–731, available at http://www.fourmilab.ch/babbage/sketch.html (viewed Nov. 28, 2007).Google Scholar
[69] Mendelson, Elliott, Second thoughts about Church's thesis and mathematical proofs, The Journal of Philosophy, vol. 87 (1990), no. 5, pp. 225–233.Google Scholar
[70] Mendelson, Elliott, On the impossibility of proving the ‘hard-half of Church's thesis, Church's thesis after 70 years (Olszewski, A., Wolenski, J., and Janusz, R., editors), Ontos Verlag, Frankfurt, 2006, pp. 304–309.Google Scholar
[71] Minsky, Marvin, Computation: Finite and infinite machines, 1st ed., Prentice-Hall, Englewood Cliffs, NJ, 1967.Google Scholar
[72] Montague, Richard, Towards a general theory of computability, Synthese, vol. 12 (1960), no. 4, pp. 429–438.Google Scholar
[73] Moschovakis, Yiannis N., What is an algorithm?, Mathematics unlimited—2001 and beyond (Engquist, B. and Schmid, W., editors), Springer-Verlag, Berlin, 2001, pp. 919–936, available at http://www.math.ucla.edu/~ynm/papers/eng.ps (viewed Nov. 28, 2007).Google Scholar
[74] Odifreddi, Plerglorglo, Classical recursion theory: The theory of functions and sets of natural numbers, Studies in Logic and the Foundations of Mathematics, vol. 125, North-Holland, Amsterdam, 1992.Google Scholar
[75] Post, Emil L., Finite combinatory processes, Formulation I, The Journal of Symbolic Logic, vol. 1 (1936), pp. 103–105, reprinted in [27], pp. 289–303.Google Scholar
[76] Post, Emil L., Absolutely unsolvable problems and relatively undecidable propositions: Account ofan anticipation, unpublished paper, 1941, in [27], pp. 340–433. Also in Solvability, provability, definability: The collected works of Emil L. Post (Davis, M., editor), Birkhäuser, Boston, MA, 1994, pp. 375–441.Google Scholar
[77] Post, Emil L., Formal reductions of the general combinatorial decision problem, American Journal of Mathematics, vol. 65 (1943), no. 2, pp. 197–215, available at doi:10.2307/2371809.Google Scholar
[78] Putnam, Hilary, Trial and error predicates and the solution to a problem of Mostowski, The Journal of Symbolic Logic, vol. 30 (1965), no. 1, pp. 49–57.Google Scholar
[79] Rabin, Michael O., Computable algebra, general theory and the theory of computable fields, Transactions of the American Mathematical Society, vol. 95 (1960), no. 2, pp. 341–360.Google Scholar
[80] Relsig, Wolfgang, On Gurevich's theorem on sequential algorithms, Acta Informatica, vol. 39 (2003), no. 5, pp. 273–305, available at http://www.informatik.hu-berlin.de/top/download/publications/Reisig2003_ai395.pdf (viewed Nov. 28, 2007).Google Scholar
[81] Rescorla, Michael, Church's Thesis and the conceptual analysis of computability, Notre Dame Journal of Formal Logic, vol. 48 (2007), no. 2, pp. 253–280.Google Scholar
[82] Rogers, Hartley Jr., Theory of recursive functions and effective computability, McGraw-Hill, New York, 1967, reprinted by MIT Press, Cambridge, MA, 1987.Google Scholar
[83] Rosser, J. Barkley, An informal exposition of proofs of Gödel's Theorem and Church's Theorem, The Journal of Symbolic Logic, vol. 4 (1939), pp. 53–60, reprinted in [27], pp. 223–230.CrossRefGoogle Scholar
[84] Rosser, J. Barkley, Highlights of the history of lambda calculus, IEEE Annals of the History of Computing, vol. 6 (1984), no. 4, pp. 337–349.Google Scholar
[85] Schönhage, Arnold, Storage modification machines, SIAM Journal on Computing, vol. 9 (1980), no. 3, pp. 490–508.Google Scholar
[86] Schroeppel, Rich, A two counter machine cannot calculate 2N , Technical Report AIM-257, A. I. Laboratory, Massachusetts Institute of Technology, Cambridge, MA, May 1972, available at ftp://publications.ai.mit.edu/ai-publications/pdf/AIM-257.pdf (viewed Nov. 28, 2007).Google Scholar
[87] Shagrir, Oron, Effective computation by humans and machines, Minds and Machines, vol. 12 (2002), no. 2, pp. 221–240, available at http://edelstein.huji.ac.il/staff/shagrir/papers/Effective_computation_by_himan_and_machine.pdf (viewed Nov. 28, 2007).Google Scholar
[88] Shapiro, Stewart, Understanding Church's thesis, Journal of Philosophical Logic, vol. 10 (1981), pp. 353–365.Google Scholar
[89] Shapiro, Stewart, Acceptable notation, Notre Dame Journal of Formal Logic, vol. 23 (1982), pp. 14–20.Google Scholar
[90] Shapiro, Stewart, Understanding Church's thesis, again, Acta Analytica, vol. 11 (1995), pp. 59–77.Google Scholar
[91] Shoenfield, Joseph R., Mathematical logic, Addison-Wesley, Reading, MA, 1967.Google Scholar
[92] Shoenfield, Joseph R., Recursion theory, Lecture Notes in Logic, vol. 1, Springer-Verlag, Berlin, 1993, reprinted by A. K. Peters, Natick, MA, 2001.Google Scholar
[93] Sleg, Wilfried, Mechanical procedures and mathematical experiences, Mathematics and mind (George, A., editor), Oxford University Press, Oxford, 1994, pp. 71–117.Google Scholar
[94] Sleg, Wilfried, Step by recursive step: Church's analysis of effective computability, this Bulletin, vol. 3 (1997), no. 2, pp. 154–180, available at http://www.math.ucla.edu/~asl/bsl/0302/0302-002.ps (viewedNov. 28, 2007).Google Scholar
[95] Sleg, Wilfried, Hilbert'sprograms: 1917–1922, this Bulletin, vol. 5 (1999), no. 1, pp. 1–44, available at http://www.math.ucla.edu/~asl/bsl/0501/0501-001.ps (viewed Apr. 21, 2008).Google Scholar
[96] Sleg, Wilfried, Calculations by man and machine: Conceptual analysis, Reflections on the foundations of mathematics: Essays in honor of Solomon Feferman (Sieg, W., Sommer, R., and Talcott, C., editors), Lecture Notes in Logic, vol. 15, A. K. Peters, Natick, MA, 2002, pp. 390–409.Google Scholar
[97] Sleg, Wilfried, Calculations by man and machine: Mathematical presentation, In the scope of logic, methodology and philosophy ofscience, vol. 1, Proceedings of the eleventh international congress of Logic, Methodology and Philosophy of Science, Cracow, Poland, August 1999 (Gärdenfors, P., Woleński, J., and Kijania-Placek, K., editors), Synthese Library, vol. 315, Kluwer Academic, Dordrecht, 2003, pp. 247–262.Google Scholar
[98] Sleg, Wilfried, Gödel on computability, Philosophia Mathematica, Series III, vol. 14 (2007), no. 2, pp. 189–207.Google Scholar
[99] Sleg, Wilfried, Church without dogma—Axioms for computability, New computational paradigms: Changing conceptions of what is computable (Cooper, S. B., Löwe, B., and Sorbi, A., editors), Springer-Verlag, Berlin, 2008, pp. 139–152. Available at http://www.hss.cmu.edu/philosophy/sieg/Church%20without%20dogma.pdf (viewed Nov. 28, 2007).Google Scholar
[100] Sleg, Wilfried, Computability: Emergence and analysis of a mathematical notion, Handbook of the philosophy of mathematics (Irvine, A., editor), to appear.Google Scholar
[101] Sieg, Wilfried and Byrnes, John, K-graph machines: Generalizing Turing's machines andarguments, Gödel96: Logical Foundations of Mathematics, Computer Science, and Physics (Hájek, P., editor), Lecture Notes in Logic, vol. 6, Springer-Verlag, Berlin, 1996, pp. 98–119.Google Scholar
[102] Sieg, Wilfried, An abstract model for parallel computations: Gandy's thesis, The Monist, vol. 82 (1999), no. 1, pp. 150–164.Google Scholar
[103] Soare, Robert I., Computability and recursion, this Bulletin, vol. 2 (1996), no. 3, pp. 284–321, available at http://www.math.ucla.edu/~asl/bsl/0203/0203-002.ps (viewed Nov. 28, 2007).Google Scholar
[104] Soare, Robert I., Computability and incomputability, Proceedings of the third conference on Computability in Europe (CiE 2007) Siena, Italy (Cooper, S. B., Löwe, B., and Sorbi, A., editors), Lecture Notes in Computer Science, vol. 4497, Springer-Verlag, Berlin, June 2007, pp. 705–715, draft available at http://www.people.cs.uchicago.edu/~soare/siena502m.pdf (viewed Nov. 28, 2007). Longer version to appear.Google Scholar
[105] Stärk, Robert, Schmid, Joachim, and Borger, Egon, Java and the Java Virtual Machine: Definition, verification, validation, Springer-Verlag, Berlin, 2001.Google Scholar
[106] Tarski, Alfred, Der Wahrheitsbegriff in den formalisierten Sprachen, Studia Philosophica, vol. 1 (1936), pp. 261–405, in German. English version: The concept of truth in formalized languages (J. H. Woodger, translator), Logic, semantics, methamathematics (J. Corcoran, editor), Hackett, Indianapolis, IN, 1983, pp. 152–277.Google Scholar
[107] Turing, Alan M., On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, Series 2, vol. 42, parts 3 and 4 (1936), pp. 230–265, Corrigenda in vol. 43 (1937), pp. 544–546. Reprinted in [27], pp. 116¬154; also in The essential Turing: Seminal writings in computing, logic, philosophy, artificial intelligence, and artificial life, plus the secrets of Enigma (B. Jack Copeland, editor), Oxford University Press, 2004, pp. 58–90; and in Collected works of A. M. Turing, vol. 4, Mathematical logic (R. O. Gandy and C. E. M. Yates, editors), North-Holland, Amsterdam, 2001, pp. 18–56. Available at http://www.abelard.org/turpap2/tp2-ie.asp (viewed Nov. 27, 2007).Google Scholar
[108] Tarski, Alfred, Computability and λ-definability, The Journal of Symbolic Logic, vol. 2 (1937), pp. 153–163, reprinted in Collected works of A. M. Turing, vol. 4, Mathematical logic (R. O. Gandy and C. E. M. Yates, editors), North-Holland, Amsterdam, 2001, pp. 59–69.Google Scholar
[109] Tarski, Alfred, Computing machinery and intelligence, Mind, vol. 59 (1950), pp. 433–460, reprinted in Collected works of A. M. Turing , vol. 1, Mechanical intelligence (D. C. Ince, editor), North-Holland, Amsterdam, 1992, pp. 133–160; and in The essential Turing (B. Jack Copeland, editor), Oxford University Press, 2004, pp. 433–464. Available at http://web.comlab.ox.ac.uk/oucl/research/areas/ieg/e-library/sources/t_article.pdf (viewedNov. 28, 2007).Google Scholar
[110] Tarski, Alfred, Solvable and unsolvable problems, Science News, vol. 31 (1954), pp. 7–23, reprinted in Collected works of A. M. Turing , vol. 1: Mechanical intelligence (D. C. Ince, editor), North-Holland, Amsterdam, 1992, pp. 187–204.Google Scholar
[111] Uspensky, Vladimir A. and Semenov, Alexei L., Algorithms: Main ideas and applications, Kluwer, Norwell, MA, 1993.CrossRefGoogle Scholar
[112] Wang, Hao, From mathematics to philosophy, Routledge and Kegan Paul, London, 1974.Google Scholar
[113] Zach, Richard, Completeness before Post: Bernays, Hilbert, and the development of propositional logic, this Bulletin, vol. 5 (1999), no. 3, pp. 331–366, available at http://www.math.ucla.edu/~asl/bsl/0503/0503-003.ps (viewed Nov. 28, 2007).Google Scholar