Re: [isabelle] Formalizing Turing machine



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






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