*To*: Randy Pollack <rpollack at inf.ed.ac.uk>*Subject*: Re: [isabelle] Object-reasoning*From*: John Munroe <munddr at gmail.com>*Date*: Sat, 25 Aug 2012 15:21:02 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CANofLe+HB23Or6AtpychKoL4_qZ5f5T1Zdymp2-PW3NiYKxgjw@mail.gmail.com>*References*: <CAP0k5J66X6sAEjuc8xbKq5mGwRPs+NZ4PatDqz8rUnO4z3E68A@mail.gmail.com> <CANofLe+HB23Or6AtpychKoL4_qZ5f5T1Zdymp2-PW3NiYKxgjw@mail.gmail.com>

Thanks, Randy. You're right that I'm not clear on the terms meta-level and object-level. So if I have, e.g., const P :: "nat => bool" lemma "P x = True" Would you say that I'm actually encoding an object-level sentence in the meta-level? That is, I'm essentially translating the object-level sentence "\forall x. P(x) = True" into Isabelle's notations, and thus "using the meta-level language only to talk about the object level". Regarding the way the object-level is represented in the meta-level and how unification in the meta-level are reflected in the object-level, that's all down to using Pure, right? A short clarification will be much appreciated. Thanks a lot for your time. John On Sat, Aug 25, 2012 at 2:48 PM, Randy Pollack <rpollack at inf.ed.ac.uk> wrote: >> Does that mean proving an object-level >> sentence involves only meta-level reasoning? > > The way you are using these words is confusing. > > The meta level should be thought of as a notation system for writing > object level syntax (terms, types, judgements, derivations, ...). > When you work in Isabelle, you are strictly only talking to the meta > level (which is Isabelle), so your sentence is "true". But you are > using the meta level language (only) to talk about the object level. > When you are working in isabelle/HOL and a lemma is accepted as > proven, you hope it really represents a lemma of (object level) HOL. > In this sense no properties of the meta level are involved except its > ability to recognize correct object level syntax. > > There is more to say, e.g. about the way the object level is > represented in the meta level, and about how proof search, > unification, etc, in the meta level are reflected in the object level. > > Randy > --- > On Sat, Aug 25, 2012 at 7:41 AM, John Munroe <munddr at gmail.com> wrote: >> Hi, >> >> Is it correct to say that there's object-level reasoning done in >> Isabelle? It seems that each step in an object-level proof is written >> using meta-level notations. Does that mean proving an object-level >> sentence involves only meta-level reasoning? >> >> Thanks a lot for your time. >> >> John >> >>

**References**:**[isabelle] Object-reasoning***From:*John Munroe

**Re: [isabelle] Object-reasoning***From:*Randy Pollack

- Previous by Date: Re: [isabelle] Are unnamed theorems used by automatic methods or Sledgehammer?
- Next by Date: Re: [isabelle] Problems with Char_ord
- Previous by Thread: Re: [isabelle] Object-reasoning
- Next by Thread: [isabelle] Weird error with locale interpretation
- Cl-isabelle-users August 2012 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