# Re: [isabelle] Formalizing Turing machine

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: Re: [isabelle] Formalizing Turing machine
*From*: Tjark Weber <webertj at in.tum.de>
*Date*: Thu, 01 Oct 2009 16:18:02 +0100
*In-reply-to*: <484D4747-C069-4492-8966-30C759670E56@cs.utah.edu>
*References*: <fb295f280909290239k28b8ce6fm1693af3d26781795@mail.gmail.com> <484D4747-C069-4492-8966-30C759670E56@cs.utah.edu>

On Wed, 2009-09-30 at 08:49 -0600, Konrad Slind wrote:
> On the face of it, even the undecidability of the Halting
> Problem seems to need sets to state (i.e. the *set* of all
> halting TMs is undecidable).
There is no need to talk about the "set of all halting TMs" to state
undecidability of the halting problem. Simply put, undecidability of
the halting problem asserts that there is no Turing machine that decides
whether an arbitrary Turing machine halts. Stating this requires
quantification over all Turing machines, but no set comprehension. (Of
course, you chose a deliberately careful wording in the first place, so
I guess this was obvious to you.)
Maybe someone else can point out the precise theory required to prove
undecidability of the halting problem?
Regards,
Tjark

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*