Logic in Computer Science (LICS 2000)

Invited Talk: From the Church-Turing Thesis to the First-Order Algorithm Theorem (at LICS 2000)

Authors: Saul A. Kripke

Abstract

This paper was conceived in reaction to Soare's paper in the Bulletin of Symbolic Logic 1996. From Gödel in the 30s, to Gandy, Soare, and many others today, the obvious fundamental importance of Turing's work both for logic and computer science has led to an overemphasis on his paper as the justification for the Church-Turing thesis. It is even said that Turing proved a theorem that every “function computable by a human being in a routine way” is Turing computable. Though several have endorsed this claim, it is hard for me to see ho w it could really meet modern standards of rigor. Moreover, Gandy worried that Turing's analysis did not cover modern computers, which may use parallel processing. He proved a very complicated result (now much simplified by Byrne and Sieg) to deal with this. My paper argues that an alternative approach {once this subject has been properly analyzed and delimited} allows us to state a simple theorem that covers computations either by machines or by humans. A thesis believed by all contemporary logicians is needed for this theorem to cover all likely future cases. It should be obvious that the theorem covers all computations known hitherto.

BibTeX

  @InProceedings{Kripke-FromtheChurchTuring,
    author = 	 {Saul A. Kripke},
    title = 	 {From the Church-Turing Thesis to the First-Order Algorithm Theorem},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {177},
    location =   {Santa Barbara, CA, USA}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }