*To*: Ramana Kumar <rk436 at cam.ac.uk>*Subject*: Re: [isabelle] Is Isabelle/Pure really a meta-logic?*From*: John Munroe <munddr at gmail.com>*Date*: Wed, 22 Aug 2012 18:34:42 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAMej=24ERc8Pgpjt+GEmWm4htmDmeLk-fF7JaqQb=3LCOUH-Yg@mail.gmail.com>*References*: <CAP0k5J5bGrsyX4exRntzOF94tm_gJ=M-u_D4Jzbm1C48mfk3MQ@mail.gmail.com> <CAMej=24ERc8Pgpjt+GEmWm4htmDmeLk-fF7JaqQb=3LCOUH-Yg@mail.gmail.com>

> > If you treat "meta-logic" and "framework logic" as synonymous, does this > problem go away? I don't think they're synonymous though. My impression is that if an object-logic is encoded within a meta-logic, then reasoning in the object-logic involves some kind of meta-level reasoning. In both cases, does the unification algorithm reason with higher-order abstract syntax? Also, is there inference in both object- and meta-levels in both cases? > > (Maybe you've heard "framework logic" used to mean something else somewhere, > though...) > Indeed. I've heard people refer to ELF as a framework logic only, whereas Gödel as a meta-logic only. John >> >> >> Thanks >> >> John >> >

**Follow-Ups**:**Re: [isabelle] Is Isabelle/Pure really a meta-logic?***From:*Lawrence Paulson

**References**:**[isabelle] Is Isabelle/Pure really a meta-logic?***From:*John Munroe

**Re: [isabelle] Is Isabelle/Pure really a meta-logic?***From:*Ramana Kumar

- Previous by Date: Re: [isabelle] Is Isabelle/Pure really a meta-logic?
- Next by Date: Re: [isabelle] Is Isabelle/Pure really a meta-logic?
- Previous by Thread: Re: [isabelle] Is Isabelle/Pure really a meta-logic?
- Next by Thread: Re: [isabelle] Is Isabelle/Pure really a meta-logic?
- 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