Re: [isabelle] Is Isabelle/Pure really a meta-logic?



On Wed, Aug 22, 2012 at 5:48 PM, John Munroe <munddr at gmail.com> wrote:

> Hi,
>
> I see that Isabelle/Pure being referred to as a meta-logic:
>
> http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols08t.pdf
>
> "The Isabelle/Pure meta-logic allows the formalization of the syntax
> and inference rules of a broad range of object-logics"
>
> and as a framework logic:
>
> http://www.cl.cam.ac.uk/research/hvg/isabelle/overview.html
>
> "These are formulated within Isabelle's logical framework
> Isabelle/Pure, which is suitable for a variety of formal calculi (e.g.
> axiomatic set theory)."
>
> My naive understanding is that a meta-logic encodes object-logics.
> Since Isabelle/Pure encodes Isabelle/HOL within it, it's a meta-logic.
> If so, how come it's called a framework logic elsewhere?
>

If you treat "meta-logic" and "framework logic" as synonymous, does this
problem go away?

(Maybe you've heard "framework logic" used to mean something else
somewhere, though...)


>
> Thanks
>
> John
>
>




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