# How does a logical framework become a meta-logical framework?

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.

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

• 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). Feb 18, 2022 at 17:58

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.

• @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: ...". Feb 25, 2022 at 18:14
• 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. Feb 25, 2022 at 18:16