*To*: "R. Pollack" <rpollack0 at gmail.com>*Subject*: [isabelle] Logical Frameworks and the Foundations of Mathematics - Re: Mathematical Logics and Logical Frameworks*From*: Ken Kubota <mail at kenkubota.de>*Date*: Thu, 3 May 2018 22:49:08 +0200*Cc*: HOL-info list <hol-info at lists.sourceforge.net>, metamath at googlegroups.com, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CANofLeL02cvMe-bhc8gEafJ=T9wLswK_3Zn85QEOLD+u+xAVOQ@mail.gmail.com>*References*: <CF58CC0D-30FF-4C70-8E0D-F92E67994B83@kenkubota.de> <CANofLeL02cvMe-bhc8gEafJ=T9wLswK_3Zn85QEOLD+u+xAVOQ@mail.gmail.com>

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: - 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: http://www.site.uottawa.ca/~afelty/HybridCoq/ 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." > 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

- Previous by Date: [isabelle] code del and code drop
- Next by Date: [isabelle] CFP: 9th International Summer School on Information Security and Protection
- Previous by Thread: Re: [isabelle] code del and code drop
- Next by Thread: [isabelle] CFP: 9th International Summer School on Information Security and Protection
- Cl-isabelle-users May 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list