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

I regard the two terms as synonymous. Larry Paulson On 22 Aug 2012, at 18:34, John Munroe <munddr at gmail.com> wrote: >> >> 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:*John Munroe

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

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

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

- 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