Re: [isabelle] Formalizing Turing machine



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.

Lawrence C Paulson
Professor of Computational Logic
Computer Laboratory, University of Cambridge
15 JJ Thomson Avenue, Cambridge CB3 0FD, England
Tel: +44(0)1223 334623    Fax: +44(0)1223 334678


On 1 Oct 2009, at 10:34, Wang Zirui wrote:

I'm sorry, but I'd like to repeat again that I'm not talking about
programming tricks. So lists are as high level as sets, because you
can implement sets by lists. Actually I don't mean sets in particular
but rather *set theory*. I want to avoid the use of sets because I
want to have nothing to do with the axioms of set theory. So lists
probably also rely on the axioms of set theory, unless you can define
it without the axioms of set theory. So let repeat my question: Can we
define Turing machine without relying on the axioms of set theory? I
think part of the misconception is because I'm posting this topic
under Isabelle. Actually my question has nothing to do with Isabelle
or HOL; I just imagined that people here might be good at formalizing
concepts and proofs using rudimentary logic theory. Sorry for the
misunderstanding.






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