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

[Timothy Y. Chow]

Alexander Zenkin <alexzen at com2com.ru> wrote:
>How is it possible that not simply mathematical theorem (Cantor's theorem
>on the uncountability of continuum), not "the intuitive meaning of the
>theorem", but its MATHEMATICAL PROOF may depend on an acceptance of the
>"vague, intuitive, philosophical" notion of "actual infinity" "what is
><certainly> not a mathematical theorem or axiom"?

Well, nowadays it is commonly believed that a necessary condition for
something to be a "mathematical proof" is that it should be clear that in
principle it can be formalized in ZFC or some such system.  Whether or not
one accepts the notion of "actual infinity," Cantor's theorem certainly
satisfies this condition, but Church's thesis (at least the version I'm
familiar with) does not.  So along with Sazonov, I'm a little puzzled as
to what the original question was asking.  The most interesting suggestion
I've seen so far is that the question was, "Can one settle the question
`Is there an effective procedure for deciding whether a Turing machine
halts?' without appealing to Church's thesis?"  This is an interesting
suggestion (not quite strictly mathematical until one specifies somewhat
more precisely what an "effective procedure" is), but is this really what
the original question was?

Tim