Email Gateway (Aug 22 2022 at 17:13): Email Gateway (Aug 22 2022 at 17:13):From: Ken Kubota <mail@kenkubota.de>
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
logic.)
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
Ken Kubota
http://doi.org/10.4444/100
Some Research Results on Logical Frameworks
Link collection:
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
http://arxiv.org/abs/0804.1879v2
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
http://www.cs.cmu.edu/~fp/papers/pldi88.pdf
Frank Pfenning (1996)
The Practice of Logical Frameworks
http://doi.org/10.1007/3-540-61064-2_33 and
http://www.cs.cmu.edu/~fp/papers/caap96.pdf
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
http://www.cs.cmu.edu/~fp/papers/cade99.pdf
Frank Pfenning (2002)
Logical Frameworks - A Brief Introduction
http://doi.org/10.1007/978-94-010-0413-8_5 and
http://www.cs.cmu.edu/~fp/papers/mdorf01.pdf
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."
Last updated: May 06 2024 at 08:19 UTC