Mathematical Logics and Logical Frameworks

Skip to first unread message

Ken Kubota

Mar 12, 2018, 3:48:42 PM3/12/18
to HOL-info list,,
Dear Members of the Research Community,

Finalizing my overview at
I would like to ask for major logics and logical frameworks not considered yet.

The logical frameworks included now (as logical frameworks, not only object
logics like Isabelle/HOL) are Isabelle and Metamath. These are also the only
two logical frameworks mentioned by Freek Wiedijk as of 2003, see p. 9 at

Kinds regards,

Ken Kubota


Ken Kubota

Ken Kubota

May 3, 2018, 4:49:18 PM5/3/18
to R. Pollack, HOL-info list,,
Hi Randy,

Thanks for your advice, which was very helpful.
In an email sent privately, somebody else also pointed out the importance of
Twelf as a logical framework system, and mentioned various logical frameworks
by Robin Adams as well as Beluga.
I have added Twelf to the graph (and a footnote on p. 3) and compiled my
research results further below.

The reason why I haven't studied the details of logical frameworks yet is that
there are two both legitimate, although conflicting methods of representing
mathematics, and logical frameworks clearly belong to the second method
(top-down), which is based on the first method (bottom-up).

For example, in Isabelle's metalogic M by Larry Paulson, the Eigenvariable
conditions appear as two distinct (independent) conditions:
"Eigenvariable conditions:
∀I: provided x not free in the assumptions
∃E: provided x not free in B or in any assumption save A", p. 19
(The object logic serving as an example here is intuitionistic first-order

By contrast, in the logic Q0 by Peter Andrews, the restrictions in these
(derived) rules have their origin in the substitution procedure of (the
primitive) Rule R', which is valid only provided that it is not the case that
"x is free in a member of [the set of hypotheses] H and free in [A = B]."
[Andrews, 2002, p. 214].
For the introduction of the universal quantifier, cf. the Rule of Universal
Generalization (Gen) (Theorem 5220 in [Andrews, 2002, p. 222]).
For the elimination of the existential quantifier, cf. Rule C (Theorem 5245 in
[Andrews, 2002, p. 230]). (Note that Andrews' Rule C covers all cases, and
Paulson's rule ∃E only the special case x=y of Rule C.)

Hence, in a bottom-up representation (like Q0) - unlike in a top-down
representation (like Isabelle's metalogic M) - it is possible to trace the
origin of the two Eigenvariable conditions back to a common root, i.e., the
restriction in Rule R'.

Generally speaking, in order to fully reveal the underlying philosophical
principles, a bottom-up representation is required, which follows the principle
of "expressiveness" (Andrews). I prefer the term "reducibility"; John Harrison
uses the term "decomposition": "complex inference rules which ultimately
decompose to these primitives"., p. 1 (PDF p. 2)

A bottom-up representation (which is better suited for foundational research)
is clearly a Hilbert-style system: It has the elegance of having only a few
rules of inference (in Q0 even only a single rule of inference - Andy Pitts:
"From a logical point of view, it would be better to have a simpler
substitution primitive, such as 'Rule R' of Andrews' logic Q0, and then to
derive more complex rules from it." [Gordon and Melham, 1993, p. 213]).
Metatheorems are not expressible within the formalism; the metatheorems are
literally "meta" ("above" - i.e., outside of - the logic). In software
implementations of Q0 or descendants (Prooftoys by Cris Perdue or my R0
implementation), the metalogical turnstile (⊢) symbol is replaced by the
logical implication, which shows the tendency to eliminate metalogical elements
from the formal language.

A top-down representation (which is better suited for applied mathematics:
interactive/automated theorem proving) is either a natural deduction system
(like HOL) or a logical framework (like Isabelle): It has a proliferation of
rules of inference (e.g., eight rules for HOL [cf. Gordon and Melham, 1993, pp.
212 f.]). Metalogical properties (metatheorems) are expressible to a certain
extent, e.g., using the turnstile (⊢) symbol (the conditionals / the parts
before the turnstile may differ in the hypothesis and the conclusion), or the
meta-implication (⇒) in Isabelle's metalogic M (not to be confused with the
implication (⊃) of the object-logic), see, p. 4
Unfortunately, the gain of expressiveness in terms of metalogical properties by
making metatheorems symbolically representable is obtained at the price of
philosophical rigor and elegance in expressing the underlying object logic
(object language).

In summary, since the top-down representations (capable of expressing
metatheorems) are based on the corresponding bottom-up representation (object
logic), the bottom-up representation has to be studied first before unraveling
further dependencies in a top-down representation. I believe Q0 or some
descendant of it to be such a basis for reducing mathematics to formal logic as
intended in Russell's philosophical program of logicism.

For the references, please see:

Best regards,



Ken Kubota

Some Research Results on Logical Frameworks

Link collection:

- Twelf's wiki:
- Abella's library:
- Beluga's distribution:
- the Coq implementation of Hybrid:

compiled from these two papers:

Amy Felty, Alberto Momigliano, Brigitte Pientka
An Open Challenge Problem Repository for Systems Supporting Binders (p. 18)

Brigitte Pientka, Joshua Dunfield
Beluga: A Framework for Programming and Reasoning with Deductive Systems
(System Description) (p. 16)

A logical framework by Robin Adams:

Robin Adams
Lambda-Free Logical Frameworks

Some interesting papers by Frank Pfenning et al.:

Frank Pfenning, Conal Elliott (1988)
Higher-Order Abstract Syntax and

Frank Pfenning (1996)
The Practice of Logical Frameworks and

Frank Pfenning, Carsten Schürmann (1999)
System Description: Twelf – A Meta-Logical Framework for Deductive Systems and

Frank Pfenning (2002)
Logical Frameworks - A Brief Introduction and

According to Pfenning and Elliott (1988), higher-order abstract syntax has an
even more expressive power than Isabelle's λ-calculus: "Isabelle [18] uses a
representation similar to ours for the statement of rules, and uses
higher-order unification for deduction. Isabelle's λ-calculus representation
does not have the expressive power of higher-order abstract syntax, but
explicitly encodes quantifier dependencies."

> Am 12.03.2018 um 23:41 schrieb R. Pollack <>:
> Ken,
> You should know about the Edinburgh Logical Framework (ELF), best implemented in the Twelf system. While ELF is a particular framework, there is tons of work about specification and programming in dependently typed frameworks. See e.g. many papers by Frank Pfenning, Amy Felty, Bob Harper, Brigitte Pientka, Alberto Momigliano. There is also a lot of work about other simply typed frameworks; e.g. Abella. There is a lot to say about consistency, expressiveness and usability of frameworks.
> You haven't even scratched the surface of logical frameworks.
> --Randy
Reply all
Reply to author
0 new messages