*To*: Jens Doll <jd at cococo.de>*Subject*: Re: [isabelle] Formalizing Turing machine*From*: Wang Zirui <zirui at nus.edu.sg>*Date*: Thu, 1 Oct 2009 17:23:57 +0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4AC456F0.80004@cococo.de>*References*: <mailman.14.1254366006.9938.cl-isabelle-users@lists.cam.ac.uk> <4AC456F0.80004@cococo.de>

But think about lambda calculus. It is computationally as powerful as Turing machine. Following your line of reasoning, it should also rely on set in its definition. But I think it's simple enough to avoid the use of set. Zirui On Thu, Oct 1, 2009 at 3:14 PM, Jens Doll <jd at cococo.de> wrote: > Churchs' thesis says, that all computability can be expressed by Turing > machines. So you probably cannot bypass sets when defining a such a > formalism. Mathematically spoken do groups, rings, (closed) fields rely on > sets in their definition. Also alphabets are sets. What do you have on mind? > Jens

**References**:**Re: [isabelle] Formalizing Turing machine***From:*Jens Doll

- Previous by Date: Re: [isabelle] Discrete Summation
- 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