FOM: The Church Thesis

[Alasdair Urquhart]

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.

Alasdair Urquhart