*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Formalizing Turing machine*From*: Wang Zirui <zirui at nus.edu.sg>*Date*: Sat, 3 Oct 2009 21:58:27 +0800*In-reply-to*: <1254488838.3940.40.camel@weber>*References*: <fb295f280909290239k28b8ce6fm1693af3d26781795@mail.gmail.com> <484D4747-C069-4492-8966-30C759670E56@cs.utah.edu> <fb295f280910010234h2192737bieb34ed72bfaa451a@mail.gmail.com> <1254488838.3940.40.camel@weber>

> http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookII/, I read a bit about proof theory. So if I want to prove from premises P_1, ..., P_k one can derive conclusion C and I used the induction principle (IND) in the proof, I'm actually showing that P_1, ..., P_k, IND entail C instead of just P_1, ..., P_k entail C. And usually for a problem whether Q_1, ..., Q_j entail D, we are actually showing Q_1, ..., Q_j, ZFC entail D.

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

**Re: [isabelle] Formalizing Turing machine***From:*Tjark Weber

- Previous by Date: Re: [isabelle] Formalizing Turing machine
- Next by Date: [isabelle] Haskell code generator problem, upper-case type variables
- 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