# Re: [isabelle] Formalizing Turing machine

Lawrence wrote:
You need to be much more specific about your research objectives and
about what you mean by set theory. Zermelo set theory is rather weak
(more or less equivalent to higher-order logic). ZF set theory is
considerably stronger, but there are set theories much stronger than
ZF. Then there is a question of the axiom of choice. Just to say "I
want to have nothing to do with the axioms of set theory" is not a
basis for a scientific discussion. People do choose to work in weak
formal systems, typically in order to investigate the power of those
systems.
Based on ZFC you can define and derive much of mathematics, so I
imagine that it's easy to define Turing machine from ZFC. The problem
with this is that it's harder to do proofs in a strong theory.
Therefore I want to define Turing machine in a weaker theory (with
fewer axioms). Basically it would good to have the theory as weak as
possible (because it facilitates proofs). But when the theory gets
weaker, it also becomes less expressive. So I want the theory to be
just strong enough to define Turing machines. I think that would be
the ideal theory, because it can express the definition of Turing
machine and it is weak enough to do certain proofs.
Zirui Wang

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