*To*: Lawrence Paulson <lp15 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:48:49 +0100*Cc*: Ramana Kumar <rk436 at cam.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <E90E39CF-B3A4-49D2-AACA-7D4E5A77EB55@cam.ac.uk>*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> <E90E39CF-B3A4-49D2-AACA-7D4E5A77EB55@cam.ac.uk>

Right. Thanks. So is there actually meta-level inference in Isabelle? The unification algorithm implemented is intended to work on object-logics, right? John On Wed, Aug 22, 2012 at 6:36 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > 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 >>>> >>> >> >

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

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

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