[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.