From: Fred Galvin
Subject: Re: countability and computability
Date: Thu, 23 Dec 1999 20:50:50 -0600
Newsgroups: sci.math
Keywords: Church-Turing thesis
On Fri, 24 Dec 1999, Jeremy Boden wrote:
> Why is the Church-Turing thesis always described as a "thesis"? I would
> infer from this that it is not a theorem in any reasonable logical
> system. I can appreciate that the halting problem is "quite tricky" but
> a thesis is generally understood to be just a defensible opinion rather
> than an accepted theorem, axiom or postulate.
The notion of (effective) computability existed, and was more or less
understood, well before any precise mathematical definition was
formulated. (The same as with such concepts as limit, function,
continuity, etc.) The Church-Turing thesis is the proposition that the
vague primordial notion of computability is correctly identified with the
precise mathematical notion of Turing-computability (or any of the various
provably equivalent notions). Historically, Church and Turing hit on their
respective theses (Church's thesis, Turing's thesis) independently, using
different but equivalent formalisms. The Church-Turing thesis can't be
proved mathematically because it asserts the equality of two things, only
one of which has a precise definition. Nevertheless, to those who believe
that the old informal notion of computability has some definite meaning,
the Church-Turing thesis is not just an arbitrary definition, but an
assumption which might be false, and could conceivably be refuted one day,
if someone comes up with a way of computing a Turing-uncomputable
function. These matters are discussed e.g. in Kleene's _Introduction to
Metamathematics_. For the views of a prominent doubter, see Laszlo Kalmar,
Arguments against the plausibility of Church's thesis, in _Constructivity
in Mathematics_, Proc. Colloq. Amsterdam 1957, pp. 72-80.
As for the unsolvability of the halting problem, that's a perfectly good
mathematical theorem; the proof (not especially tricky) is rigorous and
uncontroversial; but what is proved is that the problem can't be solved
*by a Turing machine*. If we want to interpret that to mean that the
problem is "unsolvable, period", doubters of the Church-Turing thesis may
argue that our model of computation could be inadequate.
==============================================================================
From: Neil W Rickert
Subject: Re: countability and computability
Date: 23 Dec 1999 22:12:34 -0600
Newsgroups: sci.math
Jeremy Boden writes:
>Why is the Church-Turing thesis always described as a "thesis"? I would
>infer from this that it is not a theorem in any reasonable logical
>system.
It connects the non-formal and intuitive notion of "computable" with
something strict and formal (the Turing machine). So it could not be
a theorem.
Today many people take CT as actually being the definition of
computable, which makes CT a definition, and makes the notion of
computable formal or formalizable, instead of being intuitive.
> I can appreciate that the halting problem is "quite tricky" but
>a thesis is generally understood to be just a defensible opinion rather
>than an accepted theorem, axiom or postulate.
The trickiness of the halting problem really is not involved. It is
just that a theorem cannot bridge the gap between the intuitive and
the formal.
==============================================================================
From: Gareth Rees
Subject: Re: countability and computability
Date: Fri, 24 Dec 1999 10:25:47 GMT
Newsgroups: sci.math
Jeremy Boden wrote:
> Why is the Church-Turing thesis always described as a "thesis"? I
> would infer from this that it is not a theorem in any reasonable
> logical system.
The Church--Turing thesis says, roughly, "every computable function is
computed by some Turing machine". The thesis uses the informal notion
of "computable", so is not amenable to proof.
You can even think of ways it might be falsified -- for example, if some
physical device were discovered that could carry out infinite parallel
computations.
There's also a "superthesis" which says, roughly, "all formalizations of
computation are essentially the same, in that there is a polynomial
transformation from the representation of computable functions in one
formalization to their representation in another".
--
Gareth Rees