[FOM] Re: Comment on Church's Thesis (Harvey Friedman)
V.Sazonov at csc.liv.ac.uk
Wed Jan 7 13:27:35 EST 2004
> 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
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"
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:
> Thesis licenses you to infer the absolute undecidability of the Halting
> problem from this.
More information about the FOM