Re: [isabelle] Object-reasoning



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