Re: [isabelle] Formalizing Turing machine

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.

Well, HOL is what people are typically using, and if you are new to Isabelle and are trying to use anything else, you are going to have a hard time, because other logics are much less developed in terms of tool support.

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

HOL's notion of a set is much weaker, as sets are just identified with predicates over the respective type.

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.

You can certainly try, and I think there should not be fundamental problems, but you will certainly suffer from the lack of tool support in your custom-made logic, as opposed to using something well-established.

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.

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?

The formalization is based on HOL. If you have big trouble reading the formalization, this is probably an indication that you should learn some Isabelle basics first, e.g. by working through the Tutorial (


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