FOM: The Church Thesis
urquhart at cs.toronto.edu
Mon Jan 29 16:39:05 EST 2001
The fact that the notion of computability is given
in intuitive terms does not entirely rule out a
satisfactory proof that it coincides (at least
extensionally) with a formally defined concept.
The proof could be carried out as follows.
1. Establish a set of axioms that are clearly satisfied
by the intuitive notion.
2. Show that there is a formally defined notion that satisfies
the same axioms.
3. Prove that any concept satisfying the axioms is extensionally
equivalent to the formally defined notion.
This outline of a proof was discussed on several occasions by Georg
Kreisel under the heading "informal rigour."
In the case of Church's thesis, it is perhaps questionable
whether we have a satisfactory answer to 1. Nevertheless,
in my opinion, the work of Turing, Gandy and Sieg comes
very close to fulfilling the three requirements above.
More information about the FOM