A charming discussion of what should be called the fundamental theorem of computation theory, in Epstein and Carnielli, Computability: Computable Functions, Logic, and the Foundations of Mathematics (2008):
We have studied one formalization of the notion of computability. In succeeding chapters we will study two more: recursive functions and functions representable in a formal system.
The Most Amazing Fact
All the attempts at formalizing the intuitive notion of computable function yield exactly the same class of functions.
So if a function is Turing machine computable, it can also be computed in any of the other systems described in Chapter 8.E. This is a mathematical fact which requires a proof. […] Odifreddi, 1989 establishes all the equivalences. […]
The Most Amazing Fact is stated about an extensional class of functions, but it can be stated constructively: Any computation procedure for any of the attempts at formalizing the intuitive notion of computable function can be translated into any other formalization in such a way that the two formalizations have the same outputs for the same inputs.
In 1936, even before these equivalences were established, Church said,
We now define the notion, already discussed, of an effectively calculable function of positive integers by identifying it with the notion of a recursive function of positive integers (or of a lambda-definable function of positive integers). This definition is thought to be justified by the considerations which follow, so far as positive justification can ever be obtained for the selection of a formal definition to correspond to an intuitive notion.
So we have
Church’s Thesis: A function is computable iff it is lambda-definable.
This is a nonmathematical thesis: it equates an intuitive notion (computability) with a precise, formal one (lambda-definability). By our amazing fact this thesis is equivalent to
A function is computable iff it is Turing machine computable.
Turing devised his machines in a conscious attempt to capture in simplest terms what computability is. That his model turned out to give the same class of functions as Church’s (as established by Turing in the paper cited above) was strong evidence that it was the “right” class. Later we will consider some criticisms of Church’s Thesis in that the notion of computability should coincide with either a larger or a small class than the Turing machine computable ones.