Scribd Logo
Upload

Welcome to Scribd!

  • 23 views

    Kurt Gödel and Computability Theory: Richard Zach

    Uploaded by

    klumer_x
    Kurt Gödel made several important contributions to computability theory, including his work on the decision problem, arithmetizing syntax, and showing that primitive recursive functions are representable in arithmetic. Gödel's work prompted Church and Kleene to develop arithmetic in Church's formal system and to formulate Church's thesis equating effective computability with general recursiveness. Gödel's ideas were also central to Church's theorem on the unsolvability of Entscheidungsproblem and to the development of recursive function theory.

    Copyright:

    Attribution Non-Commercial (BY-NC)
    Download as PDF, TXT or read online from Scribd

    Kurt Gödel and Computability Theory: Richard Zach

    Uploaded by

    klumer_x
    23 views17 pages
    Kurt Gödel made several important contributions to computability theory, including his work on the decision problem, arithmetizing syntax, and showing that primitive recursive functions are representable in arithmetic. Gödel's work prompted Church and Kleene to develop arithmetic in Church's formal system and to formulate Church's thesis equating effective computability with general recursiveness. Gödel's ideas were also central to Church's theorem on the unsolvability of Entscheidungsproblem and to the development of recursive function theory.

    Original Description:

    pdf

    Original Title

    cie-beam

    Copyright

    © Attribution Non-Commercial (BY-NC)

    Available Formats

    PDF, TXT or read online from Scribd

    Did you find this document useful?

    Is this content inappropriate?

    Kurt Gödel made several important contributions to computability theory, including his work on the decision problem, arithmetizing syntax, and showing that primitive recursive functions are representable in arithmetic. Gödel's work prompted Church and Kleene to develop arithmetic in Church's formal system and to formulate Church's thesis equating effective computability with general recursiveness. Gödel's ideas were also central to Church's theorem on the unsolvability of Entscheidungsproblem and to the development of recursive function theory.

    Copyright:

    Attribution Non-Commercial (BY-NC)
    Download as PDF, TXT or read online from Scribd
    Download as pdf or txt
    23 views17 pages

    Kurt Gödel and Computability Theory: Richard Zach

    Uploaded by

    klumer_x
    Kurt Gödel made several important contributions to computability theory, including his work on the decision problem, arithmetizing syntax, and showing that primitive recursive functions are representable in arithmetic. Gödel's work prompted Church and Kleene to develop arithmetic in Church's formal system and to formulate Church's thesis equating effective computability with general recursiveness. Gödel's ideas were also central to Church's theorem on the unsolvability of Entscheidungsproblem and to the development of recursive function theory.

    Copyright:

    Attribution Non-Commercial (BY-NC)
    Download as PDF, TXT or read online from Scribd
    Download as pdf or txt
    You are on page 1of 17

    Kurt Gdel and Computability Theory

    Richard Zach
    University of Calgary, Canada www.ucalgary.ca/rzach/

    CiE 2006 July 5, 2006

    Richard Zach

    Kurt Gdel and Computability Theory

    Importance of Logical Pioneers to CiE


    Wilhelm Ackermann Paul Bernays Alonzo Church Gerhard Gentzen Kurt Gdel Stephen Kleene Andrei Kolmogorov Rosza Pter Emil Post J. Barkley Rosser Kurt Schtte Thoralf Skolem Alfred Tarski Alan Turing John von Neumann
    Richard Zach Kurt Gdel and Computability Theory

    Importance of Logical Pioneers to CiE


    Wilhelm Ackermann Paul Bernays Alonzo Church Gerhard Gentzen Kurt Gdel Stephen Kleene Andrei Kolmogorov Rosza Pter Emil Post J. Barkley Rosser Kurt Schtte Thoralf Skolem Alfred Tarski Alan Turing John von Neumann 0 0 1 2 3 1 0 1 1 0 1 1 0 8 0
    Richard Zach Kurt Gdel and Computability Theory

    Gdels Legacy for Computability

    Completeness of the predicate calculus. Incompleteness of systems including arithmetic. Work on the decision problem (decidability of Gdel-Kalmr-Schtte class ). Herbrand-Gdel denition of general recursive functions. Functions reckonable in a formal system. Gdel-Gentzen translation of classical to intuitionistic logic/arithmetic. P.r. functionals of nite type (Dialectica interpretation).

    Richard Zach

    Kurt Gdel and Computability Theory

    Arithmetization of Syntax

    Gdel numbering of syntax (formulas, proofs) Showed that important functions and relations on syntax (is a formula, is a proof, substitution) are primitive recursive Showed that primitive recursive functions are numeralwise representable in Principia Showed that formulas which numeralwise represent p.r. functions are arithmetical (Gdels -function, arithmetical coding of sequences)

    Richard Zach

    Kurt Gdel and Computability Theory

    Arithmetization of Syntax

    Gdel numbering of syntax (formulas, proofs) Showed that important functions and relations on syntax (is a formula, is a proof, substitution) are primitive recursive Showed that primitive recursive functions are numeralwise representable in Principia Showed that formulas which numeralwise represent p.r. functions are arithmetical (Gdels -function, arithmetical coding of sequences)

    Richard Zach

    Kurt Gdel and Computability Theory

    Arithmetization of Syntax

    Gdel numbering of syntax (formulas, proofs) Showed that important functions and relations on syntax (is a formula, is a proof, substitution) are primitive recursive Showed that primitive recursive functions are numeralwise representable in Principia Showed that formulas which numeralwise represent p.r. functions are arithmetical (Gdels -function, arithmetical coding of sequences)

    Richard Zach

    Kurt Gdel and Computability Theory

    Arithmetization of Syntax

    Gdel numbering of syntax (formulas, proofs) Showed that important functions and relations on syntax (is a formula, is a proof, substitution) are primitive recursive Showed that primitive recursive functions are numeralwise representable in Principia Showed that formulas which numeralwise represent p.r. functions are arithmetical (Gdels -function, arithmetical coding of sequences)

    Richard Zach

    Kurt Gdel and Computability Theory

    Churchs Foundation of Logic

    Church, A set of postulates for the foundation of logic, Annals of Mathematics 1932, 1933. Developed 19291931 Gave course on it at Princeton in Fall 1931, Kleene took notes John von Neumann gave talk on Gdels 1931 incompleteness results Question: did Gdels results apply to Churchs system? Kleene tasked with developing Peano arithmetic in Churchs system

    Richard Zach

    Kurt Gdel and Computability Theory

    Consistency of Churchs System

    [. . . I]t remains barely possible that a proof of freedom from contradiction for my system can be found somewhat along the lines suggested by Hilbert. I have, in fact, made several unsuccessful attempts to do this. Dr. von Neumann called my attention last Fall to your paper entitled ber formal unentscheidbare Stze der Principia Mathematica. I have been unable to see, however, that your conclusions in 4 of this paper [on the second incompleteness theorem] apply to my system. Possibly your argument can be modied so as to make it apply to my system, but I have not been able to nd such a modication of your argument. (Church to Gdel, July 27, 1932.)

    Richard Zach

    Kurt Gdel and Computability Theory

    Peano Arithmetic in Churchs System

    Kleene, A theory of positive integers in formal logic, American J. Mathematics 1935 (work done in 1932) Denitions of numerals, +, , etc. as -terms Every primitive recursive function is -denable Used arithmetization of syntax to show that question of derivability in a formal system (e.g., Principia) is equivalent to question of whether a certain -term has a normal form

    Richard Zach

    Kurt Gdel and Computability Theory

    Gdels 1934 Princeton Course

    FebruaryMay 1934 Church, Rosser, Kleene attended Denition of general recursive functions

    Richard Zach

    Kurt Gdel and Computability Theory

    Inconsistency of Churchs System

    Kleene and Rosser, The inconsistency of certain formal logics, Annals of Mathematics 1935 (submitted 1934) Uses Gdels arithmetization of syntax to derive contradiction.

    Richard Zach

    Kurt Gdel and Computability Theory

    Churchs Theorem

    Church, An unsolvable problem of elementary number theory, American J. Mathematics 1936 -terms with normal form not -denable. Together with
    Gdels arithmetization of syntax allows representation in the system of term t has a normal form Church and Kleenes result that -denability equivalent to general recursiveness (1935), Churchs Thesis (eectively computable = general recursive), yields:

    unsolvability of decision problem of Principia. Reduced to decision problem of predicate calculus in A note on the Entscheidungsproblem, JSL 1936.

    Richard Zach

    Kurt Gdel and Computability Theory

    Recursive Function Theory

    Kleene, General recursive functions of natural numbers, Mathematische Annalen 1936 Systematic study of general recursive functions Arithmetization la Gdel of computations Kleenes T -predicate, indexes for recursive functions Normal form theorem, -recursion Construction of non-recursive functions Recursion theorem, s-m-n theorem 1938

    Richard Zach

    Kurt Gdel and Computability Theory

    Inuence of Gdel on Recursion Theory


    Prompted Church and Kleene to develop arithmetic in Churchs system Prompted development of -denability Methods used essentially to show Churchs system inconsistent -denability of p.r. functions prompted initial tentative formulation (1933) of Churchs Thesis Equivalence of -denability and general recursiveness prompted Churchs statement of Thesis in print (1936) Arithmetization of provability (via -denability) central step in Churchs Theorem Arithmetization central for basics of recursive function theory (T -predicate)
    Richard Zach Kurt Gdel and Computability Theory

    Kleene on Gdel

    After the colloquium [by von Neumann in the fall of 1931], Churchs course continued uninterruptedly concentrating on his formal system; but on the side we all read Gdels paper, which to me opened up a whole new world of fascinating ideas and perspectives.

    Richard Zach

    Kurt Gdel and Computability Theory

    You might also like