Email Gateway (Aug 19 2022 at 08:22): Email Gateway (Aug 19 2022 at 08:22):From: John Munroe <munddr@gmail.com>
Hi,
I see that Isabelle/Pure being referred to as a meta-logic:
http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols08t.pdf
"The Isabelle/Pure meta-logic allows the formalization of the syntax
and inference rules of a broad range of object-logics"
and as a framework logic:
http://www.cl.cam.ac.uk/research/hvg/isabelle/overview.html
"These are formulated within Isabelle's logical framework
Isabelle/Pure, which is suitable for a variety of formal calculi (e.g.
axiomatic set theory)."
My naive understanding is that a meta-logic encodes object-logics.
Since Isabelle/Pure encodes Isabelle/HOL within it, it's a meta-logic.
If so, how come it's called a framework logic elsewhere?
Thanks
John
Email Gateway (Aug 19 2022 at 08:22):From: Ramana Kumar <rk436@cam.ac.uk>
On Wed, Aug 22, 2012 at 5:48 PM, John Munroe <munddr@gmail.com> wrote:
Hi,
I see that Isabelle/Pure being referred to as a meta-logic:
http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols08t.pdf
"The Isabelle/Pure meta-logic allows the formalization of the syntax
and inference rules of a broad range of object-logics"and as a framework logic:
http://www.cl.cam.ac.uk/research/hvg/isabelle/overview.html
"These are formulated within Isabelle's logical framework
Isabelle/Pure, which is suitable for a variety of formal calculi (e.g.
axiomatic set theory)."My naive understanding is that a meta-logic encodes object-logics.
Since Isabelle/Pure encodes Isabelle/HOL within it, it's a meta-logic.
If so, how come it's called a framework logic elsewhere?
If you treat "meta-logic" and "framework logic" as synonymous, does this
problem go away?
(Maybe you've heard "framework logic" used to mean something else
somewhere, though...)
Thanks
John
Email Gateway (Aug 19 2022 at 08:22):From: John Munroe <munddr@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
Email Gateway (Aug 19 2022 at 08:22):From: Lawrence Paulson <lp15@cam.ac.uk>
I regard the two terms as synonymous.
Larry Paulson
Email Gateway (Aug 19 2022 at 08:22):From: John Munroe <munddr@gmail.com>
Right. Thanks.
So is there actually meta-level inference in Isabelle? The unification
algorithm implemented is intended to work on object-logics, right?
John
Email Gateway (Aug 19 2022 at 08:22):From: Randy Pollack <rpollack@inf.ed.ac.uk>
---------- Forwarded message ----------
From: Randy Pollack <rpollack0@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@gmail.com>
Cc: Lawrence Paulson <lp15@cam.ac.uk>, Ramana Kumar <rk436@cam.ac.uk>,
cl-isabelle-users@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
Email Gateway (Aug 19 2022 at 08:22):From: Lawrence Paulson <lp15@cam.ac.uk>
Also called a meta-logical-framework. I prefer that name as being more uniform.
Larry
Email Gateway (Aug 19 2022 at 08:23):From: Steve Wong <s.wong.731@gmail.com>
Regarding the remark about higher-order abstract syntax, should one call
the Term datatype in Term.ML HOAS? If I understand correctly, Its purpose
is to bind the meta-language to the the object-language.
Cheers
Steve
Last updated: Apr 23 2024 at 04:18 UTC