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

[Vladimir Sazonov]

addamo wrote:
> 
> I don't understand how your comment refers to Church's Thesis.
> Could you make it more explicit?
> 
> Do you or anybody know a proof of the undecidability of the Halting problem
> not depending on Church's Thesis?


Sorry, how is it possible that any mathematical theorem (such as 
the undecidability of the Halting problem) may depend on anything 
what is not a mathematical theorem or axiom (like Church's Thesis 
which is not a mathematical statement)? 

Of course, the intuitive meaning of a theorem may depend on some 
intuitive (informal) considerations. 

By the way, as to CT, if we will consider 
Bounded Arithmetic + \neg EXP where EXP means that 
exponential is total function, then we can still define 
in this theory what is Turing Machine (with some minor, 
but essential precaution) and prove existence of the 
universal TM, s-m-n, recursion theorem, the undecidability 
of the corresponding Halting problem, etc. (Of course, 
TM computing 2^n will not halt!) In the underlying 
imaginary world of such a version of BA we could argue 
quite plausibly that TM define "exactly" all computable 
functions. (Just another version of CT.) Even 2^n is 
computable, however partial. This is also intuitively 
sufficiently plausible by reference to the real computer 
practice. 

In the case of BA with sharply bounded quantifiers 
we can also consider its Heyting version (analogous 
to Heyting Arithmetic HA), Kleene realizability, 
formal CT, Markov's principle, and the whole ordinary 
theory concerning these concepts (although, with some 
peculiarities). Consistency of the formal CT with this 
arithmetic confirms again that in this exponentialless 
world (here - intuitionistic world) TM define "all" 
computable functions. 

These considerations are here to state that CT or any 
other informal statement like "epsilon-delta definition 
of continuity corresponds to our intuition sufficiently 
well" (even despite some well known counterexamples) 
may have in principle many variations and have only 
informal and not any absolute character in principle. 

This statement contrasts with the opinion of Aatu Koskensilta: 

> Church's
> Thesis licenses you to infer the absolute undecidability of the Halting 
> problem from this.

Vladimir Sazonov

> 
> Adam