*To*: Wang Zirui <zirui at nus.edu.sg>*Subject*: Re: [isabelle] Formalizing Turing machine*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Wed, 30 Sep 2009 12:06:41 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <fb295f280909300225k55f35315r608a8f03d719e661@mail.gmail.com>*References*: <fb295f280909290239k28b8ce6fm1693af3d26781795@mail.gmail.com> <4AC31798.7080205@in.tum.de> <fb295f280909300225k55f35315r608a8f03d719e661@mail.gmail.com>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20090701)

Dear Zirui,

The point of not relying on ZFC is because it's a strong theory. I don't want the definition of Turing machine to be based on a strong theory. I want it to be based on a theory that is as weak as possible. So it's best if it's based on nothing.

Unfortunately HOL is at least as strong as ZFC because it has the idea of a set.

My teacher Jain suggests that it might be possible to define Turing machine based on Peano Arithmetic, which is weaker than ZFC. And I'm going to try that.

I don't understand the AFP formalization of automata as I read it. Does the author use the idea of sets, functions or numbers? If yes, he probably base the definition of automata on HOL or ZFC. But I want to base it on a weaker theory. Does the author do that?

Alex

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

**Re: [isabelle] Formalizing Turing machine***From:*Alexander Krauss

**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 September 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