Re: [isabelle] Object-reasoning



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
>>
>>





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