[isabelle] Logical Frameworks and the Foundations of Mathematics - Re: Mathematical Logics and Logical Frameworks

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"
        http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf, 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".
        http://www.cl.cam.ac.uk/~jrh13/papers/reflect.pdf, 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
        http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf, 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: http://doi.org/10.4444/100.111

Best regards,



Ken Kubota

Some Research Results on Logical Frameworks

Link collection:

- Twelf's wiki: http://twelf.org/wiki/Case_studies
- Abella's library: http://abella-prover.org/examples
- Beluga's distribution: http://complogic.cs.mcgill.ca/beluga/
- 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
http://doi.org/10.4204/EPTCS.185.2 (p. 18)

Brigitte Pientka, Joshua Dunfield
Beluga: A Framework for Programming and Reasoning with Deductive Systems 
(System Description)
http://doi.org/10.1007/978-3-642-14203-1_2 (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
http://doi.org/10.1145/53990.54010 and 

Frank Pfenning (1996)
The Practice of Logical Frameworks
http://doi.org/10.1007/3-540-61064-2_33 and 

Frank Pfenning, Carsten Schürmann (1999)
System Description: Twelf – A Meta-Logical Framework for Deductive Systems
http://doi.org/10.1007/3-540-48660-7_14 and 

Frank Pfenning (2002)
Logical Frameworks - A Brief Introduction
http://doi.org/10.1007/978-94-010-0413-8_5 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 <rpollack0 at gmail.com>:
> 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
> On Mon, Mar 12, 2018 at 7:48 PM, Ken Kubota <mail at kenkubota.de> wrote:
> Dear Members of the Research Community,
> Finalizing my overview at http://www.owlofminerva.net/files/fom.pdf
> 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
>         http://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf
> Kinds regards,
> Ken Kubota
> ____________________
> Ken Kubota
> http://doi.org/10.4444/100

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.