\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

Metalogical Frameworks

Table of Contents

1. Introduction

Whereas a Logical Framework is used to encode a logic so we can emulate reasoning within it, a Metalogical Framework encodes a logic so we can prove metatheorems concerning it.

In particular a metalogical framework consists of an underlying logical framework such that it can prove metatheorems. For example, proving cut-elimination.

I will often write "meta-logical framework" and "metalogical framework" interchangeably.

2. Examples of Meta-Logical

HOL is a meta-logical framework, since it can encode judgements using inductive types (thanks to the Tarski-Knaster theorem) and inference rules using implication. We can then state metatheorems in a straightforward manner using induction. This suffices to make HOL a meta-logical framework.

A NON-example is Automath, which is too weak to prove metatheorems.

A mixed example would be Isabelle (which is a fragment of intuitionistic higher-order logic) alone is insufficient to be a meta-logical framework. But Isabelle/HOL is a meta-logical framework, since HOL is a meta-logical framework.

3. Defining Metalogical Frameworks

We can transform any logical framework into a meta-logical framework by encoding a meta-logical framework into our given logical framework. This is precisely what Isabelle did with HOL.

But viewed category theoretically, this would suggest that a meta-logical framework consists of a logical framework equipped with some extra structure (and possibly extra properties), wouldn't it?

Clavel and Meseguer have stressed the importance of reflection principles in establishing a deductive system is a metalogical framework. (For more about reflection principles, see John Harrison's review, especially §§3 et seq.)

3.1. Observation: Weakly Constructive

It seems that all meta-logical frameworks are "weakly constructive" (see, e.g., section 5.3 of HOL Light's manual). Basin and Constable argued in their paper defining metalogical frameworks that a deductive system needs to be "suitable constructive or computational" for it to be even a candidate as a meta-logical framework.

However, this property ("weakly constructive") may be accidental and inessential. It is unclear to me at present.

3.2. Observation: Initial Model

Basin, Clavel, and Meseguer argue in "Reflective Metalogical Frameworks":

A logic's syntax and proofs are inductively built from syntax and proof constructors. A logical framework and a metalogical framework can share these as a common basis. However, […], for a metalogical framework the representation must additionally preserve the inductive nature of the syntax and proof constructors. Model-theoretically, this means that a formalization in the metalogic should have an initial model, which corresponds to the syntax and proofs of the formalized object logic.

This is admittedly persuasive…at least, I cannot imagine reasoning about a logic without an inductive representation of its syntax and semantics, which would be equivalent to this "initial model" condition. Thus it seems unavoidable that the "initial model" condition is necessary.

One thing worth noting is that, when we allow initial models, we are really allowing for a "deep embedding" of the "object logic" in the logical framework. This is what allows us to state and prove metatheorems concerning the "object logic". I learned this fact (initial models allow proving metatheorems) from:

  • Jacob Prinz, G Kavvos, Leonidas Lampropoulos,
    "Deeper Shallow Embeddings". In 13th International Conference on Interactive Theorem Proving (ITP 2022), 2022, Eprint.

The idea of an "initial model" isn't new or novel, it's been around for 50 years (or longer). See the "initial model theorem" as discussed on the Stanford Encyclopedia of Philosophy entry on first-order model theory; see also §1.6.5, §§2.2.3 et seq of Jacobs' book on Categorical Logic (which seems to use similar notation as the articles cited for our source of discussion of metalogical frameworks).

Basically, an equation is true in the initial model if and only if it is true in an arbitrary model. That's why we care about initial models, that's why encoding an "object logic" as an initial syntactic model is important, that's why we care about "deep embeddings". José Meseguer really pioneered pointing this out in the domain of semantics for programming languages, see his paper, "Relating Models of Polymorphism" (POPL 1989, pp.228–241) for references.

4. Logical Frameworks via Reflection Principles

The criteria which seems to be subject to fierce debate is whether a meta-logical framework obeys reflection principles or not. "Reflection" is a relatively "soft" concept (like predicativity).

4.1. Entailment System

In logic, we have a notion of a "first-order language" built atop the logic. The "space of first-order languages" is then generalized as an "entailment system", which codifies a notion of provability or entailment, is defined as:

An Entailment System consists of

  • \(\mathbf{Sign}\) a category of signatures

equipped with

  • \(sen\colon\mathbf{Sign}\to\mathbf{Set}\) a functor associating to each signature \(\Sigma\) a corresponding set of $Σ$-sentences
  • \(\vdash\) a function mapping a signature [object] \(\Sigma\in\mathbf{Sign}\) a binary relation \(\vdash_{\Sigma}\subset\mathcal{P}(sen(\Sigma))\times sen(\Sigma)\)

such that

  1. Reflexivity: for any \(\varphi\in sen(\Sigma)\), \(\{\varphi\}\vdash_{\Sigma}\varphi\)
  2. Monotonicity: if \(\Gamma\vdash_{\Sigma}\varphi\) and \(\Gamma\subset\Gamma'\), then \(\Gamma'\vdash_{\Sigma}\varphi\)
  3. Transitivity: if \(\Gamma\vdash_{\Sigma}\varphi_{j}\) for all \(j\in I\), and \(\Gamma\cup\{\varphi_{j}\mid j\in J\}\vdash_{\Sigma}\psi\), then \(\Gamma\vdash_{\Sigma}\psi\),
  4. \(\vdash\) translation: if \(\Gamma\vdash_{\Sigma}\varphi\), then for any \(H\colon\Sigma\to\Sigma'\) in \(\mathbf{Sign}\), \(sen(H)(\Gamma)\vdash_{\Sigma'}sen(H)(\varphi)\), where \(sen(H)(\Gamma)=\{sen(H)(\varphi)\mid\varphi\in\Gamma\}\).

We can meaningfully discuss a notion of proof calculi for entailment systems. See §2.3 of "Axiomatizing Reflective Logics and Languages" by Manuel G. Clavel & Jose Meseguer (Eprint).

Signature morphisms in the underlying category \(\mathbf{Sign}\) may be from including a signature \(\Sigma\) into a larger signature \(\Sigma'\), or from changing syntax, or something similar.

Let \(\mathcal{E}\) be an entailment system. We define its category \(\mathbf{Th}\) of Theories to consist of

objects
pairs \(T = (\Sigma,\Gamma)\) of a signature \(\Sigma\) and \(\Gamma\subset sen(\Sigma)\)
morphisms
\(H\colon(\Sigma,\Gamma)\to(\Sigma',\Gamma')\) consists of a signature morphism \(H\colon\Sigma\to\Sigma'\) such that if \(\varphi\in\Gamma\), then \(\Gamma'\vdash_{\Sigma'}sen(H)(\varphi)\).

There is also the forgetful functor \(sign\colon\mathbf{Th}\to\mathbf{Sign}\), and the induced functor \(sen\colon\mathbf{Th}\to\mathbf{Set}\) given by \(sen(T)=sen(sign(T))\).

I believe this means that \(\mathbf{Th}\) is fibred over \(\mathbf{Sign}\).

4.2. Using Institutions

Basin, Clavel, and Meseguer's "Reflective Metalogical Frameworks" formalizes model theory using institutions. This is a common way to formalize model theory beyond first-order logic, and has been used in the literature since their introduction in the '70s.

An Institution consists of

  • \(\mathbf{Sign}\) a category whose objects are called "signatures"

equipped with

  • \(sen\colon\mathbf{Sign}\to\mathbf{Set}\) a functor assigning to each signature its set of $Σ$-sentences;
  • \(\mathbf{Mod}\colon\mathbf{Sign}\to\mathbf{Cat}^{op}\) is a [contravariant] functor that assignts to each signature a category whose objects are called $Σ$-models; and
  • a function \(\vDash\) associating to each signature \(\Sigma\in\mathbf{Sign}\) a binary relation \(\vDash_{\Sigma}\subset\mathrm{Ob}(\mathbf{Mod}(\Sigma))\times sen(\Sigma)\) called $Σ$-satisfaction

such that

  • the satisfication condition holds: for each \(H\colon\Sigma\to\Sigma'\) in \(\mathbf{Sign}\), for each model \(M'\in\mathbf{Mod}(\Sigma')\) and every \(\varphi\in sen(\Sigma)\), we have \(M'\vDash_{\Sigma'}sen(H)(\varphi)\iff\mathbf{Mod}(H)(M')\vDash_{\Sigma}\varphi\).

We can also note, if \(T=(\Sigma,\Gamma)\) is a theory, its model category \(\mathbf{Mod}(T)\) is the full subcategory of \(\mathbf{Mod}(\Sigma)\) determined by the models \(M\in\mathbf{Mod}(\Sigma)\) which satisfy all the sentences in \(\Gamma\) — i.e., for each \(\varphi\in\Gamma\), we have \(M\vDash_{\Sigma}\varphi\).

Given an institution \(I\), we may construct an entailment system \(I^{+}\) where we construct the relation: \(\Gamma\vdash_{\Sigma}\varphi\) if and only if \(M\vDash_{\Sigma}\varphi\) for every \(M\in\mathbf{Mod}(T)\) for \(T=(\Sigma,\Gamma)\).

4.3. Logic = Entailment System + Institution

A logic can now be defined in glorious generality as a sound institutionalized entailment system.

A Logic consists of

  • \(\mathbf{Sign}\) a category whose objects are called "signatures"

equipped with

  • \(sen\colon\mathbf{Sign}\to\mathbf{Set}\) a functor associating to each signature \(\Sigma\) a corresponding set of $Σ$-sentences
  • \(\vdash\) a function mapping a signature [object] \(\Sigma\in\mathbf{Sign}\) a binary relation \(\vdash_{\Sigma}\subset\mathcal{P}(sen(\Sigma))\times sen(\Sigma)\)
  • \(\mathbf{Mod}\colon\mathbf{Sign}\to\mathbf{Cat}^{op}\) is a [contravariant] functor that assignts to each signature a category whose objects are called $Σ$-models; and
  • a function \(\vDash\) associating to each signature \(\Sigma\in\mathbf{Sign}\) a binary relation \(\vDash_{\Sigma}\subset\mathrm{Ob}(\mathbf{Mod}(\Sigma))\times sen(\Sigma)\) called $Σ$-satisfaction

such that

  1. it forms an entailment system with \((\mathbf{Sign}, sen, \vdash)\)
  2. it forms an institution with \((\mathbf{Sign}, sen, \mathbf{Mod}, \vDash)\)
  3. Soundness condition: for each \(\Sigma\in\mathbf{Sign}\), \(\Gamma\subset sen(\Sigma)\), and \(\varphi\in sen(\Sigma)\), we have \(\Gamma\vdash_{\Sigma}\varphi\implies\Gamma\vDash_{\Sigma}\varphi\), where \(\Gamma\vDash_{\Sigma}\varphi\) holds if and only if \(M\vDash_{\Sigma}\varphi\) holds for any model \(M\) that satisfies all the sentences in \(\Gamma\).

Given an institution \(I\), we can construct an entailment system \(I^{+}\) and together these form a logic, which is denoted \(I^{\dagger}\) (or, by an abuse of notation, use a superscript "plus"…which is more common). Furthermore, this logic is complete.

4.4. Relevant Reflection Principles

Then the particular notion of reflection can be described as:

Given an entailment system \(\mathcal{E}\) and a nonempty set of theories \(\mathcal{C}\) in it, a theory \(U\) is \(\mathcal{C}\) Universal if there is an injective function (called a "representation function")

\begin{equation} \overline{(-\vdash-)}\colon\bigcup_{T\in\mathcal{C}}(\{T\}\times sen(T))\to sen(U) \end{equation}

such that for each \(T\in\mathcal{C}\), \(\varphi\in sen(T)\),

\begin{equation} T\vdash_{sign(T)}\varphi\iff U\vdash_{sign(U)}\overline{T\vdash\varphi}. \end{equation}

If further \(U\in\mathcal{C}\), we call the entailment system \(\mathcal{E}\) \(\mathcal{C}\) Reflective.

Finally, we define a Reflective Logic to be a logic whose entailment system is \(\mathcal{C}\) reflective for \(\mathcal{C}\) the classof all finitely presentable theories in the logic.

4.5. Logical Framework

From this perspective, we may thus define a logical framework as:

A Logical Framework consists of

  • a logic \(\mathcal{L}\)
  • a theory \(U\) in the class \(\mathcal{C}\) of finitely presentable theories of \(\mathcal{L}\)

such that \(U\) is $\mathcal{C}$-universal.

This observation seems to have also been made in §3 of "Axiomatizing Reflective Logics and Languages" by Manuel G. Clavel & Jose Meseguer (Eprint). In particular, what we would typically refer to as a "logical framework", they denote by the universal theory \(U\).

5. Definition of Meta-logical Framework

Let me give a "morally right" definition, which fails to be rigorous:

A Meta-logical framework consists of a logical framework \((\mathcal{L}, \mathcal{C}, U)\) equipped with

  • a super logic \(\mathcal{S}\) containing \(\mathcal{L}\subset\mathcal{S}\) [the term is analogous to how a "superset" contains a "subset", don't think of something like Supermathematics with Grassmann algebras]

such that

  1. Super-nice super-logic: the logic \(\mathcal{S}\) is "suitably nice" (has Tarskian semantics and admits universal & existential quantification).
  2. Initiality: for each theory \(T\in\mathcal{C}\), there exists an initial model \(\mathcal{I}(T)\in\mathbf{Mod}(T)\).
  3. Inductive proofs: for each theory \(T\in\mathcal{C}\), there is an extension \(U\subset Ind(U)\) in \(\mathcal{S}\) such that we can do inductive proofs with \(Ind(U)\) concerning the metatheory of any \(T\).

It's not clear exactly how super-nice the superlogic has to be; is there something weaker than having Tarskian semantics?

Also, it's unclear when will a logic \(\mathcal{L}\) have a superlogic \(\mathcal{S}\) which has Tarskian semantics and admits quantifiers.

Can we reformulate this notion of a metalogical framework within the more familiar judgements and inference rules setting?

6. References

  • David A. Basin and Robert L. Constable,
    "Metalogical frameworks".
    Logical Environments (1993) pp.1–29. Eprint
    • This seems to be the first paper which invented the term "metalogical framework".
  • D. Basin, and M. Clavel, and J. Meseguer,
    "Reflective metalogical frameworks".
    ACM Transactions on Computational Logic 5, no.3 (2004) pp.528–576. Eprint
  • David Basin and Manuel Clavel and José Meseguer,
    "Rewriting logic as a metalogical framework".
    In International Conference on Foundations of Software Technology and Theoretical Computer Science, pp. 55-80. Springer, Berlin, Heidelberg, 2000.

6.1. Logic, Entailment Systems, etc.

  • J Meseguer,
    "General logics".
    In Logic Colloquium'87 (H.-D. Ebbinghaus et al., Eds.) North-Holland, Amsterdam, The Netherlands, 275–329. Eprint

6.2. Principle of Reflection

  • Manuel Clavel and José Meseguer,
    "Axiomatizing reflective logics and languages".
    In Proceedings of Reflection, vol. 96, pp. 263-288. 1996; Eprint
  • John Harrison,
    "Metatheory and Reflection in Theorem Proving: A Survey and Critique".
    Technical Report CRC-053, SRI International Cambridge Computer Science Research Centre, 1995. Eprint

6.3. Using HOL

  • Petros Papapanagiotou and Jacques Fleuriot,
    "Object-Level Reasoning with Logics Encoded in HOL Light".
    arXiv:2101.03808, 17 pages.

Last Updated 2023-03-09 Thu 09:16.