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

Logical Framework

Table of Contents

1. Introduction

The basic idea of a logical framework is that we want to:

  • describe a given logic (from a large class of deductive systems)
  • emulate reasoning within the aforementioned logic

This is all rather vague, since "deductive system" is vague (and if we try to make the notion more precise, we tend to omit important systems). But a large class of deductive systems may be described in terms of judgements and inference rules.

From this perspective, a logical framework is then a metalanguage with some prescribed manner to encode a judgement (sometimes denoted using the Oxford brackets \([\![J]\!]\) for the encoding of the judgement \(J\)) and inference rules.

If we try to make this more precise, then we commit ourselves to a particular foundation (i.e., to a particular logical framework). I'll just discuss two particular popular families of logical frameworks.

1.1. Adequacy Theorem

Usually, the critical steps when working with a logical framework amounts to:

  1. Write down the judgements and inference rules for your "object logic"
  2. Devise an encoding for them in your logical framework
  3. Prove your encoding is adequate (i.e., there is a bijection between the object logic and the encoded version), so that valid proofs using the encoded system corresponds to valid proofs in the "object logic"

This notion of adequacy seems to be introduced by Honsell, Plotkin, and Harper's paper "Framework for defining logics". In practice, this amounts to producing a so-called Adequacy Theorem to prove we have a bijection. For an example of this "in the wild", see Harper and Licata's "Mechanizing Metatheory in a Logical Framework" (viz., §3).

2. Dependent Types

Historically, this was the first way logical frameworks emerged, specifically in de Bruijn's Automath. If we wanted to encode a logic \(L\) in dependent type theory, we start with a judgement in \(L\) like

\begin{equation} \Gamma\vdash_{L}\varphi \end{equation}

We begin by defining primitive notions of the logic in Automath (or the dependently-typed lambda calculus) \(\bar\Gamma_{L}\), then we have some encoding \(T(\varphi)\) of the judgement \(\varphi\) and an encoding \(T(\Gamma)\) of the context, and we have now to produce a proof term \(p\) of the encoded judgement-as-type:

\begin{equation} \bar\Gamma_{L}, T(\Gamma)\vdash_{LF} p : T(\varphi) \end{equation}

Harper, Honsell, and Plotkin make this rigorous in their LF type theory.

3. Higher-Order Logic

Following Paulson's "Foundation of a Generic Theorem Prover" (see §3, definition 1) we can encode a logic in higher-order logic, where we add some primitive definitions to the logical framework \(\mathcal{M}\) to get \(\mathcal{M}_{L}\), a way to encode judgements \(J\) as formulas \([\![J]\!]\), and inference rules

\begin{equation} \frac{J_{1}\quad\dots\quad J_{n}}{J}C \end{equation}

with side condition(s) \(C\), premises \(J_{1}\), …, \(J_{n}\), and conclusion \(J\), may be encoded as an implication:

\begin{equation} [\![C]\!]\implies([\![J_{1}]\!]\implies[\dots\implies([\![J_{n}]\!]\implies [\![J]\!])]). \end{equation}

This suffices to provide a framework for encoding any judgement of the deductive system, and reasoning within that deductive system.

4. Open Questions

Here are some open questions (to me), and I'd be interested if anyone has solutions.

Question 1: Define "logic". A logical framework "encodes" a "logic", but I have not seen "logic" rigorously defined anywhere. What can be encoded? What can't be?

It seems the consensus (either explicitly or implicitly) is: a logic is a system described by judgements and inference rules. I think this intersects are large number of logics, and there are a large number of systems (described by judgements and inference rules) which are not logics. Is this description "optimal" in the sense that it's pithy and supports "enough" systems of logic that refining it further produces a baroque definition that's unworkable in practice?

Question 2: Can different logical frameworks support disjoint sets of logics? Presuming there is some "sufficient" definition from the previous question, does a logical framework need to be able to encode all of the logics? Or can a logical framework encode a large subset of logics? In the latter case, can different logical frameworks encode disjoint subsets of logics? What's the relationship between facets of logical frameworks and the encodable logics?

Question 3: Can FOL + \(\mathsf{ZF}^{++}\) be a logical framework? Can we use first-order logic and set theory as a logical framework? I haven't seen anyone say it's possible (conversely, I haven't seen anyone say it's impossible either).

(I am facetiously referring to "some suitable set theory" as \(\mathsf{ZF}^{++}\), analogous to C++.)

5. References

  • N. G. de Bruijn,
    "A survey of the project Automath".
    In Selected Papers on Automath, PDF
  • R. Harper, F. Honsell and G. Plotkin,
    "A Framework for Defining Logics".
    In Symposium on Logic in Computer Science, 1987, pages 194-204; Eprint
  • Lawrence Paulson,
    "The Foundation of a Generic Theorem Prover".
    arXiv:cs/9301105, 37 pages.
  • Robert Harper and Daniel R. Licata,
    "Mechanizing Metatheory in a Logical Framework".
    Journal of functional programming 17, no. 4-5 (2007) pp.613–673.

Last Updated 2022-02-22 Tue 08:31.