What is the difference between logical framework and type theory? Both of them have types, terms, and are based on dependently typed lambda calculus.

We have Edinburg LF which is based on lambda-pi calculus, however, it seems to me that there's some subtle difference there.


Summary. A logical framework is a meta-language for the formalisation of deductive systems, where deductions become syntactic objects.

Of course what counts as a meta-language is quite vague, and it is helpful to understand the historical development of logical frameworks. The first logical framework was de Bruijn's Automath (1), which is based on $\lambda$-calculus. Many of the ideas from the Automath language family have found their way into modern logical frameworks. Martin-Löf's work on constructive type-theories, also based on $\lambda$-calculi, has also been influential.

Edinburgh's LF (2) is a very influential logical framework. Edinburgh LF is what you get when you enrich the simply typed $\lambda$-calculus with type-dependency. That's all. In order to make type-dependency precise, one needs to replace the function space operator $A \rightarrow B$ on types with type-abstraction, usually written $\Pi x^A. B$, and introduce the kind of types, as well as kind abstraction. In terms of rules, the key is in the elimiation rule for $A \rightarrow B$, resp. $\Pi x^A. B$:

$$ \newcommand{\TYPES}[3]{#1 \vdash #2 : #3} \newcommand{\SUBST}[2]{\{#1/#2\}} \frac{ \TYPES{\Gamma}{\color{red}{M}}{A \rightarrow B} \qquad \TYPES{\Gamma}{\color{red}{N}}{A} }{ \TYPES{\Gamma}{\color{red}{MN}}{B} } \qquad \frac{ \TYPES{\Gamma}{{\color{red}M}}{\Pi x^A. B} \qquad \TYPES{\Gamma}{\color{red}{N}}{A} }{ \TYPES{\Gamma}{{\color{red}{MN}}}{B\SUBST{{\color{red}N}}{x}} } $$

On the left we have the rule for the simply typed $\lambda$-calculus, on the right the rule that generalises the left with type dependency. We see that a value 'flows' into the type in the conclusion on the right.

I think the interactive proof assistant Isabelle uses intuitionistic second order logic based on $\lambda$-calculus, without any numbers or recursive data types as logical framework. Various others have been proposed.

One advantage of using $\lambda$-calculi as logical framework is that binding constructs like universal quantifiers can be implemented using the framework's $\lambda$-binder. Note that most logical frameworks are expressively weak: the frameworks support object-level reasoning, but are insufficient to perform much meta-theoretic reasoning beyond the fact that a particular object-level statement is a theorem. In fact the metal-logic is usually so weak that even proving the deduction theorem for a Hilbert-style object logic is impossible. Of course nothing prevents you from using more powerful type-theories as a logical framework.

For these practical and historical reasons, most logical frameworks in use today are typed $\lambda$-calculi, i.e. type-theories. See (3, 4) for more in-depth discussions of logical frameworks.

  1. N. de Bruijn: The Mathematical Language AUTOMATH, Its Usage, and Some of Its Extensions.

  2. R. F. Harper, F. Honsell, G. Plotkin: A Framework for Defining Logics.

  3. F. Pfenning: Logical frameworks.

  4. F. Pfenning: Logical frameworks -- A Brief Introduction.

  • $\begingroup$ Do you know about any introductory books about proof assistants (logical frameworks) suitable for someone who already know basics of simply typed lambda calculus and first order logic? $\endgroup$ – Trismegistos Feb 19 '15 at 10:19
  • 1
    $\begingroup$ @Trismegistos I'm afraid I don't. I suggest to learn a specific assistant. Agda is the easiest to get into as it's basically Haskell, but with dependent types. In my experience, the logical framework is not as important as other dimensions of proof assistants. For example Isabelle is a generic prover that you can instantiate with different logics, so really exposes the logical framework. But Isabelle/HOL is the only instantiation used in practise. This is because all proof tactics, all prover support has been written for the HOL object logic. And usability of a prover depends on those. $\endgroup$ – Martin Berger Feb 19 '15 at 10:27

Your Answer

