Re: [isabelle] Formalizing Turing machine
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
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