Email Gateway (Aug 22 2022 at 14:20): Email Gateway (Aug 22 2022 at 14:20):From: Ken Kubota <mail@kenkubota.de>
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).
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
Last updated: Apr 25 2024 at 04:18 UTC