# [isabelle] Formalizing Turing machine

Hi,
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.
Yes, in the definition of Turing machine we see sets, such as the set
of states, but I think the use of set is convenient but not necessary.
(Am I wrong?) So if you agree with me and think it's possible to go
without sets, could you please outline how to define Turing machine?
If you think this is impossible, can you give a proof?
Thanks.
Regards,
Zirui Wang

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