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. ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
