9
$\begingroup$

In a recent answer, Isabelle was noted as a Logical Framework.
A comment noted it was a Meta-Logical Framework.

In researching for an understanding found

"Logical and Meta-Logical Frameworks" by Frank Pfenning (pdf)

Slide 2

Some Terminology

Deductive System: Calculus of axioms and inference rules defining derivable judgments. Used in the presentation of logics and programming languages.

Logical Framework: Meta-language for the formalization of deductive system.

Meta-Logical Framework: Meta-language for reasoning about deductive systems.

Slide 4

Some Logical Frameworks

  • Implementations: Isabelle, ...

Slide 6

Some Meta-Logical Frameworks

  • General-purpose reasoning systems used as meta-logical frameworks (... Isabelle/HOL, ...)

At this point I could not form a consistent understanding between the comment and these slides.

So clarification was asked in the comments and one was provided.

Now it is time to pay the so called bill by asking the question so points can be given.

$\endgroup$
1
  • $\begingroup$ I've written a couple draft answers, but I'm not satisfied with any of them. I'll re-examine them after work (i.e., in 5 hours or so). $\endgroup$ Commented Feb 18, 2022 at 17:58

1 Answer 1

2
$\begingroup$

Let me try taking a stab at a few provisional definitions. I can make these arbitrarily rigorous, but being fully general makes it hard to see the forest for the trees (at least, for me).

Provisional Definition 1. A "Logical Framework" consists of a sufficiently strong meta-language capable of (1) specifying any deductive system, and (2) reasoning within a deductive system. (End of Provisional definition 1)

Technically, a logical framework is not "just" a meta-language, but a logic. We use it to simulate derivations in a given deductive system.

Provisional Definition 2. A "Meta-logical Framework" consists of a logical framework whose underlying metalanguage is capable of proving theorems concerning the deductive systems encoded by the logical framework. (End of provisional definition 2)

In particular, meta-logical frameworks form a proper subset of logical frameworks.

A sufficient condition for a logical framework to be a meta-logical framework is:

  1. Have an inductive encoding of an object logic, and
  2. Be capable of doing proofs by induction.

I say "sufficient" because, of all the meta-logical frameworks we currently have, they're all described by these extra conditions.

Example 1. HOL is a metalogical framework. We can construct inductive datatypes in a variety of ways, e.g., using Tarski's fixed point theorem. Poofs by structural induction are then straightforward.

(Aside: using Tarski's fixed point theorem to encode inductive types is actually impredicative; John Harrison has a predicative alternative.)

Non-Example 2. Isabelle/pure is a fragment of intuitionistic higher-order logic which only allows "Hereditary Harrop Formulas", which precludes adequate proofs of induction.

Example 3. Any categorical logic seems to have sufficient strength to be a metalogical framework.

Example 4. If $\mathcal{L}$ is a logical framework, and $\mathcal{M}$ is a metalogical framework, then we can encode $[[-]]\colon\mathcal{M}\to\mathcal{L}$ the metalogical framework into the logical framework. This let's us "transport" the ability to prove metatheorems into a logical framework, because we're using it to "emulate" a meta-logical framework. (This is what Isabelle did with Isabelle/HOL.)

Concluding remarks. Here is normally where I list off the references for further reading, but the only adequate papers about meta-logical frameworks work within Meseguers' "General Logics" framework (pdf) (rather than with Martin-Lof's judgements), which adds a couple hundred pages of preliminary reading before getting to the meat of the matter...and even then, it's spread across a few papers spanning a couple hundred pages. So I do not know if you are up for reading ~500 pages just to learn more about meta-logical frameworks.

$\endgroup$
2
  • $\begingroup$ @GuyCoder the criteria given in "Rewriting Logic..." has 3 items; the first condition [being sufficiently reflective] is precisely the same as stating a meta-logical framework must be a logical framework. If you think about it for a moment, it makes sense, since "reasoning within a deductive system" is a weaker demand than "proving metatheorems about a deductive system". To see this, you could state the meta-theorem, "The following reasoning is valid in deductive system X: ...". $\endgroup$ Commented Feb 25, 2022 at 18:14
  • $\begingroup$ Clavel and Meseguer's Axiomatizing Reflective Logics and Languages works out a bit of this in some detail, discussing how reflective proof calculi is capable of "emulating" any deductive system within the given class of logics. $\endgroup$ Commented Feb 25, 2022 at 18:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.