*To*: John.Harrison at cl.cam.ac.uk*Subject*: [isabelle] The HOL family, HOL Light, Q0, and type abstraction*From*: Ken Kubota <mail at kenkubota.de>*Date*: Mon, 24 Oct 2016 02:49:11 +0200*Cc*: OndÅej KunÄar <kuncar at in.tum.de>, Andrei Popescu <a.popescu at mdx.ac.uk>, "Prof. Michael J. C. Gordon" <mjcg at cl.cam.ac.uk>, "Prof. Thomas F. Melham" <thomas.melham at balliol.ox.ac.uk>, cl-isabelle-users at lists.cam.ac.uk, Roger Bishop Jones <rbj at rbjones.com>, "Prof. Peter B. Andrews" <andrews at cmu.edu>, Cris Perdue <cris.perdue at gmail.com>, Rob Arthan <rda at lemma-one.com>, "Prof. Andrew M. Pitts" <Andrew.Pitts at cl.cam.ac.uk>, "Professor William M. Farmer" <wmfarmer at mcmaster.ca>, HOL-info list <hol-info at lists.sourceforge.net>, Mark Adams <mark at proof-technologies.com>*In-reply-to*: <E1by9Df-0005MD-4F@mta1.cl.cam.ac.uk>*References*: <E1by9Df-0005MD-4F@mta1.cl.cam.ac.uk>

Hi John, Cris, Mark, Rob, and Roger, Before going into the details of John's e-mail on the motivation for HOL Light, from which I included a larger passage, let me reply to the other comments concerning the overview at http://dx.doi.org/10.4444/100.111 The following paragraph was added (plus a list of links): "Neither the graph nor the above list are comprehensive. Further logics are William M. Farmer's Q0u and Q0uqe (extensions of Andrews' Q0 with undefinedness), and further systems are TPS by Peter B. Andrews et al., HOL Zero by Mark Adams (designed for trustworthiness, and rather a proof checker like Automath and the R0 implementation), and IMPS by William M. Farmer et al. (with partial functions and subtypes). Historically, "[t]he original LCF team at Stanford consisted of Robin Milner, assisted by Whitfield Diffie" [Gordon, 2000, p. 169] - now known for the Diffie-Hellman (DH) key exchange in cryptography. Both Rob Arthan and Roger Bishop Jones generously credit each other for having the main rÃle in the creation of ProofPower." It's difficult to add more systems to the graph. Further are included in the new list and are in good company with Andrews' TPS, which I hesitated to add to the graph, as it would distract from the much more important Q0. Due to the suggestions of Rob Arthan, I have included a footnote for HOL with the three references given. I am not sure whether the mechanism is already implemented in HOL4, see section 2.5.5 of http://freefr.dl.sourceforge.net/project/hol/hol/kananaskis-10/kananaskis-10-logic.pdf In case the article on Isabelle/HOL by Ondrej Kuncar and Andrei Popescu will be printed again elsewhere, I would like to suggest two modifications of the part quoted in my overview: 1. Gordon's proposal was rather in the eighties than in the nineties (release of HOL88 in 1988, Gordon's technical report of 1985). 2. The formulation "Classical Higher-Order Logic" seems the be more common than "Classic Higher-Order Logic". Thanks to Cris Perdue, Mark Adams, Rob Arthan, and Roger Bishop Jones for the hints. If you still miss any important information, please do not hesitate to send a notice via the mailing lists. John's e-mail on the motivation for HOL Light and his comparison with Andrews' systems is highly interesting. I would suggest an article "On the Logical Foundations of HOL Light" or similar to make the information persistent, as the policy of the mailing list provider may change. For now, I have quoted from the publicly available e-mail via the online link. I totally agree that the derivation of higher-order logic (and of mathematics in general) on the basis of the notion of equality is "quite satisfying". When I met Andrews, he told me that he chose the letter 'Q' in the name of his system Q0 because it is based on the notion of equality. For philosophical reasons, I would prefer the word 'identity', but mathematically it doesn't make a difference. As most people do not look behind the definitions (e.g., of the quantifiers), these definitions first might look "intricate", but logically they are simply the result of spelling out their inner logic (i.e., following Andrews' concept of "expressiveness", which I also call "reducibility"). In higher-order logic, where propositions are not a separate syntactic category anymore, the "conventional notation âx. P[x] [maps] down to â(Îx. P[x])". https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf (p. 218), or similarly http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf (p. 10). With type abstraction, also types are not a separate syntactic category anymore, but terms of type tau. Then the quantifiers have the type as an argument, such that the expression is not just ALL (\x. P[x]), but ALL t (\x. P[x]), where 't' is the type (or a type variable), meaning "for all x of type t, P holds", for example ALL t (\z.((x z) => (y z))) in the definition of the subset or ALL o (\x.(g x)) in Axiom 1 of R0 (Law of Excluded Middle, like Axiom 1 of Q0), see: http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (p. 357) http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf (p. 351) I much appreciate that in HOL Light the basic logical notions including the quantifiers are independent of the "suspicious" epsilon operator. Eventually, maybe with the introduction of type abstraction (already suggested by Gordon), in the HOL systems the epsilon operator should be eliminated and replaced by the description operator, as in Andrews' Q0. For example, Gordon's definition of "the conditional term Cond" in Gordon's 2001 paper at http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.6103&rep=rep1&type=pdf (p. 24) can be replaced by Andrews' definition of C, see Andrews' theorem 5313 and its formal verification (here with type abstraction) at http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf (pp. 165 ff.) Thank you very much for this interesting information, John. Best, Ken ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100 > Am 23.10.2016 um 05:13 schrieb John.Harrison at cl.cam.ac.uk: > > Hi Ken, > > I have a few remarks about the HOL Light foundations. Part of my > objective in HOL Light was to arrive at a simpler and more satisfying > logical kernel that could nevertheless be the foundation of a > practical tool. In particular HOL Light's foundations address a couple > of the issues on which you quoted some self-criticism from the HOL > documentation: the complicated primitive substitution rule and on the > way the epsilon operator is plumbed deep into the foundations. On the > first point: > > "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/Melham, 1993, > p. 213] > > The HOL Light foundations do exactly that, adopting just simple 1-step > congruence rules MK_ABS and MK_COMB together with reflexivity, > symmetry and transitivity of equality. Although the traditional SUBST > rule is also present, it is not a primitive and in fact has rather an > involved derivation. > > In addition to Pitts' insight, the use of the description operator > (like in Andrews' Q0) should be preferred to the use of the epsilon > operator (used by Gordon, who already called it "suspicious"), > > In HOL Light the basic logical notions including the quantifiers are > all defined independent of the epsilon operator (in contrast to its > use even to define "there exists" in the original HOL). The choice > operator is eventually introduced but it is quite late. If you look > at the sequence of "load" operations in the root file: > > https://github.com/jrh13/hol-light/blob/master/hol.ml > > the epsilon operator only appears in the file "class.ml" after some > development of logical derived rules including those for automating > inductive definitions. > > Ultimately, all the quantifiers and connectives in HOL Light are > defined in terms of equality alone. In this respect the foundations > are reminiscent of one of Andrews's systems, but with the distinction > that the definitions are intuitionistically admissible. (The type > definition principle is not quite intuitionistically acceptable in its > present form, but it could be made so.) Actually, it is only when the > epsilon operator is introduced that the Law of Excluded Middle is > deduced as a consequence, via a simplification due to Mark Adams of > the classic Diaconescu proof. One could alternatively introduce a > definite descriptor and much of the later material would still work > in this context. > > I think there is something quite satisfying about the derivation of > higher-order logic from these simple foundations based just on > equality in a simple world of functions. Of course, one may find it > rather artificial to use these intricate definitions of quantifiers, > instead of taking them as basic which, to greater or lesser extent, > other HOL variants do. Nevertheless, it turns out that HOL Light's > foundations match almost perfectly a standard presentation of the > internal logic of a topos. This was a coincidence and I only became > aware of it when Konrad Slind pointed it out, but it provides some > kind of support for choices I made on the general grounds of > intellectual simplicity. I remember my astonishment when Konrad > pointed me at sec II.2 of Lambek and Scott's "Intro to Higher-order > categorical logic" where you find the HOL Light deductive system > almost exactly, even down to the slightly less natural rule I call > DEDUCT_ANTISYM_RULE (basically antisymmetry of implication in the > context of |- not ==>). Cf the Wikipedia page which has a nice summary > of the basic rules: > > https://en.wikipedia.org/wiki/HOL_Light > > There is a bit more historical material about the way HOL Light and > its relatives evolved near the end of the HOL Light tutorial, starting > around p216: > > https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf > > John.

- Previous by Date: Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?
- Next by Date: [isabelle] New AFP article: Stable Matching
- Previous by Thread: [isabelle] Smash flex-flex pairs in calculational reasoning
- Next by Thread: [isabelle] New AFP article: Stable Matching
- Cl-isabelle-users October 2016 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