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