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

On Thu, 2009-10-01 at 17:34 +0800, Wang Zirui wrote: > I'm sorry, but I'd like to repeat again that I'm not talking about > programming tricks. So lists are as high level as sets, because you > can implement sets by lists. Actually I don't mean sets in particular > but rather *set theory*. I want to avoid the use of sets because I > want to have nothing to do with the axioms of set theory. So lists > probably also rely on the axioms of set theory, unless you can define > it without the axioms of set theory. So let repeat my question: Can we > define Turing machine without relying on the axioms of set theory? Turing machines are finite objects. They can be encoded as numbers (via some Gödel numbering, cf. http://en.wikipedia.org/wiki/G%C3%B6del_number). So depending on what you want to prove exactly, and provided that you don't want to speak about (infinite) sets of Turing machines, you may indeed be able to avoid set theory entirely, and merely work in (some fragment of) a theory of arithmetic (cf. http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookII/, http://en.wikipedia.org/wiki/Robinson_arithmetic, http://en.wikipedia.org/wiki/Peano_arithmetic). Since your teacher suggested this in the first place, why not ask him to explain the details? Note that finite lists (of numbers) can be encoded as numbers (again, via some Gödel numbering), so they are not "as high level as sets". Also note that Alex was perfectly right when he wrote: | If these foundational issues of taking the weakest logic possible are | really the core of your interest, then you can try and go for Peano | Arithmetic, but if your main interest is formalizing Turing Machines | after all, then using anything but HOL is like cutting your left leg | off before climbing a mountain. If you really want to restrict yourself to Peano arithmetic, I suspect that a formalization on paper (not using Isabelle) would already be enough of a challenge for a small student project. Regards, Tjark

**Follow-Ups**:**Re: [isabelle] Formalizing Turing machine***From:*Wang Zirui

**References**:**Re: [isabelle] Formalizing Turing machine***From:*Wang Zirui

- Previous by Date: Re: [isabelle] Formalizing Turing machine
- Next by Date: Re: [isabelle] Formalizing Turing machine
- Previous by Thread: Re: [isabelle] Formalizing Turing machine
- Next by Thread: Re: [isabelle] Formalizing Turing machine
- Cl-isabelle-users October 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list