*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Fwd: Is Isabelle/Pure really a meta-logic?*From*: Randy Pollack <rpollack at inf.ed.ac.uk>*Date*: Wed, 22 Aug 2012 14:11:08 -0400*In-reply-to*: <CANofLeJRWT+Nf1Wn+nBSnKnfi4mpUs3bD3udfYsAHaZ4UeVfxA@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> <E90E39CF-B3A4-49D2-AACA-7D4E5A77EB55@cam.ac.uk> <CAP0k5J6nEgz19-kgUX108DfZhpezz-5LDMQas1NyTmAS8FKCDg@mail.gmail.com> <CANofLeJRWT+Nf1Wn+nBSnKnfi4mpUs3bD3udfYsAHaZ4UeVfxA@mail.gmail.com>*Sender*: rpollack0 at gmail.com

---------- Forwarded message ---------- From: Randy Pollack <rpollack0 at gmail.com> Date: Wed, Aug 22, 2012 at 2:07 PM Subject: Re: [isabelle] Is Isabelle/Pure really a meta-logic? To: John Munroe <munddr at gmail.com> Cc: Lawrence Paulson <lp15 at cam.ac.uk>, Ramana Kumar <rk436 at cam.ac.uk>, cl-isabelle-users at lists.cam.ac.uk The terms are frequently used differently. A framework logic is a very weak metalogic. A framework logic is a formal setting for constructing the syntax (terms, types, judgements, derivations, ...) of an object language, but not to reason about them; i.e. no induction in the framework over the syntax of the object logic. Isabelle is a framework logic in this sense. A metalogic formalizes the construction of the syntax of the object logic, usually as true inductive objects, allowing induction over the construction of these objects. The distinction is not so simple. E.g. Twelf is based on a framework (Edinburgh Logical Framework), but by meta-reasoning about the Framework itself, Twelf achieves some ability to reason about object syntax. Randy -- On Wed, Aug 22, 2012 at 1:48 PM, John Munroe <munddr at gmail.com> wrote: > 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

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