Encyclopedia

Logical framework

Wikipedia contributorsAdapted for Fathomly · View authors

2 min read
Source updated March 24, 2026

In logic, a logical framework provides a means to define (or present) a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for (interactive) automated theorem proving. The first logical framework was Automath; however, the name of the idea comes from the more widely known Edinburgh Logical Framework, LF. Several more recent proof tools like Isabelle are based on this idea. Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.

01Overview

A logical framework is based on a general treatment of syntax, rules and proofs by means of a dependently typed lambda calculus. Syntax is treated in a style similar to, but more general than Per Martin-Löf's system of arities.

To describe a logical framework, one must provide the following:

A characterization of the class of object-logics to be represented;
An appropriate meta-language;
A characterization of the mechanism by which object-logics are represented.

This is summarized by:

"Framework = Language + Representation."

02LF

In the case of the LF logical framework, the meta-language is the λΠ-calculus. This is a system of first-order dependent function types which are related by the propositions as types principle to first-order minimal logic. The key features of the λΠ-calculus are that it consists of entities of three levels: objects, types and kinds (or type classes, or families of types). It is predicative, all well-typed terms are strongly normalizing and Church-Rosser and the property of being well-typed is decidable. However, type inference is undecidable.

A logic is represented in the LF logical framework by the judgements-as-types representation mechanism. This is inspired by Per Martin-Löf's development of Kant's notion of judgement, in the 1983 Siena Lectures. The two higher-order judgements, the hypothetical $J\vdash K$ and the general, $\Lambda x\in J.K(x)$ , correspond to the ordinary and dependent function space, respectively. The methodology of judgements-as-types is that judgements are represented as the types of their proofs. A logical system ${\mathcal {L}}$ is represented by its signature which assigns kinds and types to a finite set of constants that represents its syntax, its judgements and its rule schemes. An object-logic's rules and proofs are seen as primitive proofs of hypothetico-general judgements $\Lambda x\in C.J(x)\vdash K$ .

An implementation of the LF logical framework is provided by the Twelf system at Carnegie Mellon University. Twelf includes

a logic programming engine
meta-theoretic reasoning about logic programs (termination, coverage, etc.)
an inductive meta-logical theorem prover

Watch videos about Logical frameworkExplainers and documentaries on YouTube (opens in a new tab)

Sources and credits

This article is adapted from the Wikipedia article “Logical framework”, written by its contributors and licensed under CC BY-SA 4.0. Fathomly has changed the layout, removed citation markers, navigation and maintenance notices, and adjusted punctuation. This adapted version is shared under the same license. For references, see the original article.

Fathomly is not affiliated with or endorsed by the Wikimedia Foundation. Spotted a problem? Tell us.

Logical framework

01Overview

02LF

Sources and credits

Related topics

Grammatical Framework (programming language)

Turnstile (symbol)