*To*: Wang Zirui <zirui at nus.edu.sg>*Subject*: Re: [isabelle] Formalizing Turing machine*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Fri, 2 Oct 2009 12:36:14 +0100*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>, Konrad Slind <slind at cs.utah.edu>*In-reply-to*: <fb295f280910010234h2192737bieb34ed72bfaa451a@mail.gmail.com>*References*: <fb295f280909290239k28b8ce6fm1693af3d26781795@mail.gmail.com> <484D4747-C069-4492-8966-30C759670E56@cs.utah.edu> <fb295f280910010234h2192737bieb34ed72bfaa451a@mail.gmail.com>

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.

**References**:**Re: [isabelle] Formalizing Turing machine***From:*Wang Zirui

- Previous by Date: Re: [isabelle] Polymorphic parameter in locales
- Next by Date: Re: [isabelle] Formalizing Turing machine
- Previous by Thread: Re: [isabelle] Formalizing Turing machine
- Next by Thread: Re: [isabelle] Formalizing Turing machine
- Cl-isabelle-users October 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list