[FOM] Re: Comment on Church's Thesis (Harvey Friedman)

[Timothy Y. Chow]

On Mon, 12 Jan 2004, Alexander M Lemberg wrote:
> Is Church's Thesis not exactly such a specification?

No, it is the Turing machine that is one possible specification.  Church's
Thesis says that out of all possible specifications that you might
imagine, this is the correct one.  So it says something like

"Turing machine = effective algorithm"

To formalize this sentence we need to formalize both sides.  The left-hand
side is easy, but what about the right-hand side?  If you use the same
syntactic string on the right as on the left, then you get a trivial
identity of the form "x = x" and clearly this does not capture the meaning
of Church's thesis---and in particular there's no sense in which "x = x"
is fundamentally "used" in any undecidability proof.

The standard view is that the right-hand side is not formalizable, any
more than the right-hand side of the following sentence is formalizable:

"Turing machine = coolest idea since sliced bread"

Even a rabid fan of the Turing machine concept, who firmly believes the
Sliced Bread Thesis, would not claim that the Sliced Bread Thesis is
formalizable in ZFC (or whatever).

Possibly one could come up with an axiomatic definition of "effective
algorithm" that is not trivially equivalent to the definition of a Turing
machine, and then one could formalize Church's Thesis and ask for a proof
of it.  Shoenfield worked on this for a while, I am told, but didn't get
very far.  It's also what I was obliquely referring to in the message of
mine that you quoted.  Anyway, this is a slightly nonstandard point of
view.

Tim