[isabelle] Formalizing Turing machine


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?


Zirui Wang

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