Kripke's Alleged Proof of Church-Turing Thesis: A Critical Analysis

On Kripkes Alleged Proof of Church-Turing Thesis Chen Long 2018/10/19

Outline of the Talk 1.The received view of CTT 2. Some recent attempts to prove it 3. Kripke s new proof 4. A Comparison with Church s argument

1. The Received View of CTT An essentially unprovable thesis rather than a theorem: While we cannot prove Church s thesis, since its role is to delimit precisely an hitherto vaguely conceived totality, we require evidence that it cannot conflict with the intuitive notion which it is supposed to complete. (Kleene, 1952, p. 318)

Evidence for CTT The most amazing confluence: Alonzo Church, 1936, An unsolvable problem of elementary number theory; Stephen Kleene, 1936, General recursive functions of natural numbers; Alan Turing, 1936, On computable numbers, with an application to the Entscheidungsproblem; Emil Post, 1936, Finite combinatory processes. Formulation ;

Formalism-free: G del 1946: the importance is largely due to the fact that with this concept one has for the first time succeeded in giving an absolute definition of an interesting epistemological notion, i.e., one not depending on the formalism chosen. In all other cases treated previously, such as definability, one has been able to define them only relative to a give language demonstrability or

Turings Original Argument: I: A direct appeal to intuition II: A proof of the equivalence of two definitions (in case the new definition has a greater intuitive appeal) [Turing s provability theorem] III: Giving examples of large classes of numbers which are computable Turing s own view: all arguments which can be given are bound to be, fundamentally, appeals to intuition, and for this reason rather unsatisfactory mathematically

2. Some recent attempts to prove it Reservations about CTT as a pure thesis : (a) Asymmetrical treatment of CTT (b)The possibility of a disproof

The axiomatic method: Church 1935: My proposal that lambda- definability be taken as a definition of it (effective computability) he (G del) regarded as thoroughly unsatisfactory. His only idea at the time was that it might be possible, in terms of effective undefined notion, to state a set of axioms which would embody the generally accepted properties of this something on that basis. calculability as an notion, and to do

Dershowitz, N., & Gurevich, Y. (2008). A Natural Axiomatization of Computability and Proof of Church s Thesis. The Bulletin of Symbolic Logic, 14(3), 299 350. Sieg, W. (2008). Church Without Dogma: Axioms for Computability. In B. Cooper (Ed.), New Computational Paradigms (pp. 139 152). New York: Springer.

3. Kripkes New Proof Kripke, S. (2013). The Church-Turing Thesis as a Special Corollary of G del s Completeness Theorem. In Computability: Turing, G del, Church, and Beyond (pp. 77 104).

Premise 1: Computation as a special form of deduction computation mathematical argument. One is given a set of instructions, and the steps in the computation are supposed to follow follow deductively from the instructions computation is just another mathematical deduction, albeit one of a very specialized form. is a special form of as given. So a

Premise 2: Hilberts Thesis The steps of any mathematical argument can be given in a language based on first-order logic (with identity) From premise 1 and 2, we can get C(1): Every (human) computation can be formalized as a valid deduction couched in the language of first-order language with identity.

Applying Gdels completeness theorem to C(1) then yields the conclusion that: C(2): Every (human) computation is provable in first-order predicate calculus with identity, in the sense that, given an appropriate formalization, each step of the computation can be derived from the instructions (possibly with some other auxiliary premises)

Together with Turings provability theorem [Every formula provable in Hilbert s first-order predicate calculus can be proved by the universal Turing machine] which Kripke takes to be the main point of Turing s argument II, we then get: C(3): Every (human) computation can be done by Turing machine (CTT)

4: Comparison with Churchs Argument Church s step-by-step argument: F is effectively calculable if and only if there is an expression f in the logic L such that f(u)=v is a theorem of L iff F(m)=n; here, u and v are expressions that stand for the positive integers m and n.

Some conditions any system of logic has to satisfy if it is to serve at all the purposes for which a system of symbolic logic is usually intended : (1) each rule must be an effectively calculable operation, (2) the set of axioms and rules (if infinite) must be effectively enumerable. Church s interpretation: (a) each rule must be recursively enumerable, (b) the set of rules and axioms must be recursively enumerable, and (c) the relation between a positive integer and the expression which stands for it must be recursive.

Churchs Central Thesis: The steps of any effective procedure (governing proofs in a system of symbolic logic) must be recursive. Church s Thesis= Church s Central Thesis+ Theorem of general recursive functions

The stumbling block in Churchs Step by step argument: The fatal weakness in Church s argument, however, is the core assumption that the atomic steps were stepwise recursive, something he did not justify but only taken dogmatically

Thank you!