[Hol-info] The HOL family, HOL Light, Q0, and type abstraction

[Ken K. <ma...@ke...>]

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 Joh...@cl...:
> 
> 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.