Editing Church–Turing thesis (section)

== Informal usage in proofs ==

Proofs in computability theory often invoke the Church–Turing thesis in an informal way to establish the computability of functions while avoiding the (often very long) details which would be involved in a rigorous, formal proof.<ref>Horsten in {{harvcolnb|Olszewski|Woleński|Janusz|2006|page=256}}.</ref> To establish that a function is computable by Turing machine, it is usually considered sufficient to give an informal English description of how the function can be effectively computed, and then conclude "by the Church–Turing thesis" that the function is Turing computable (equivalently, partial recursive).

Dirk van Dalen gives the following example for the sake of illustrating this informal use of the Church–Turing thesis:<ref>{{harvcolnb|Gabbay|2001|page=284}}</ref>

{{quote|1=Example: Each infinite [[recursively enumerable]] (RE) set contains an infinite [[recursive set]].

Proof: Let A be infinite RE. We list the elements of A effectively, n<sub>0</sub>, n<sub>1</sub>, n<sub>2</sub>, n<sub>3</sub>, ...

From this list we extract an increasing sublist: put m<sub>0</sub>&nbsp;= n<sub>0</sub>, after finitely many steps we find an n<sub>k</sub> such that n<sub>k</sub> > m<sub>0</sub>, put m<sub>1</sub>&nbsp;= n<sub>k</sub>. We repeat this procedure to find m<sub>2</sub> > m<sub>1</sub>, etc. this yields an effective listing of the subset B={m<sub>0</sub>, m<sub>1</sub>, m<sub>2</sub>,...} of A, with the property m<sub>i</sub> < m<sub>i+1</sub>.

''Claim''. B is decidable. For, in order to test k in B we must check if k&nbsp;= m<sub>i</sub> for some i. Since the sequence of m<sub>i</sub>'s is increasing we have to produce at most k+1 elements of the list and compare them with k. If none of them is equal to k, then k not in B. Since this test is effective, B is decidable and, '''by Church's thesis''', recursive.}}

In order to make the above example completely rigorous, one would have to carefully construct a Turing machine, or λ-function, or carefully invoke recursion axioms, or at best, cleverly invoke various theorems of computability theory. But because the computability theorist believes that Turing computability correctly captures what can be computed effectively, and because an effective procedure is spelled out in English for deciding the set B, the computability theorist accepts this as proof that the set is indeed recursive.