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



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





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