Re: [isabelle] Formalizing Turing machine

Hi Alex,

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?

Your suggestion of automata is certainly good as it has the same
problem as Turing machines, but it's simpler.


On Wed, Sep 30, 2009 at 4:32 PM, Alexander Krauss <krauss at> wrote:
> Deac Zirui,
>> I'd like to formalize the definition of Turing machine. If possible,
>> I'd like to do it without relying on ZFC. That is, I don't use sets,
>> integers and so on.
> There should be no problems with doing it in HOL. Note that HOL also has a
> notion of a set, although it is not quite the same as in ZFC.
>> [...] So if you agree with me and think it's possible to go
>> without sets, could you please outline how to define Turing machine?
> You may want to look at Tobias Nipkow's formalization of finite automata,
> which you can find in the AFP:
> It's not Turing Machines, but it may give you an idea...
> Alex

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