Hi John,
I have read both papers
http://www.cl.cam.ac.uk/~jrh13/papers/joerg.html
http://www.cl.cam.ac.uk/~jrh13/papers/holright.html
and will include them in the overview.
Let me comment on "HOL Done Right" first before discussing "History of
Interactive Theorem Proving" and the connection to the paper by Kuncar and
Popescu.
1. "Slind has added type quantifiers as suggested by Melham (1992) [...]" (p. 1)
I am not aware of HOL4 (or any other HOL implementation by Konrad Slind)
implementing type quantifiers - please let me know if I have overlooked
something.
Also, maybe Tom could comment on whether his 1992 article significantly differs
from his 1993 article available online at
http://www.cs.ox.ac.uk/tom.melham/pub/Melham-1994-HLE.pdf
drawing on Andrews' system Q from 1965 with quantification over types.
Both articles have identical names and roughly the same page count:
http://dx.doi.org/10.1016/B978-0-444-89880-7.50007-3 (Melham 1992)
http://dx.doi.org/10.1007/BF01383982 (Melham 1993)
2. "Note that Henkin (1963) showed how all the logical constants could be
derived classically from just a higher order function calculus." (p. 7)
It's interesting that you refer to Henkin's article in Fundamenta Mathematicae
52 (1963) available online at
http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52123.pdf
with errata at
http://matwbn.icm.edu.pl/ksiazki/fm/fm53/fm53125.pdf
whereas my first main reference is the article directly following in the same
volume, i.e., Andrews' article, which simplifies Henkin's axiom system and
marks the birth of Q0 (1963), available online at
http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52124.pdf
and quoted at
http://dx.doi.org/10.4444/100.111
I still have the print Peter Andrews gave me.
For me, it is also interesting to see that the names of Rule R and Rule T,
which I mainly know from Andrews' second (2002) edition, have their origin in
Henkin's article of 1963 ("Rule of Replacement" / "Rule R", p. 330; "Rule T",
p. 332).
3. "If we were really interested in parsimony, every logical operation could be
defined, and the turnstile regarded as a logical operator." (p. 7)
Actually, this is done in R0.
In the effort of expressing everything _within_ the object language (not being
dependent on a metatheory), the turnstile was eliminated and replaced by the
implication.
Accordingly, Andrews Rule R' [Andrews, 2002, p. 214] was reformulated in R0.
As discussed earlier at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00069.html
(section 4)
I consider Rule R' (and not Rule R) as the main rule, as it also takes into
account a possible set of hypotheses, and Rule R may be viewed as only a
special case of R' (with an empty set of hypotheses).
In HOL, according to Andy Pitts, there are "three primitive constants":
equality (identity), epsilon operator, and implication
http://freefr.dl.sourceforge.net/project/hol/hol/kananaskis-10/kananaskis-10-logic.pdf
(p. 21)
In Q0/R0, of course, the epsilon operator is replaced by the description
operator.
In addition to that, it has to be admitted that despite the claim that "Q0
requires [...] only two basic constants (identity/equality and its counterpart,
description)"
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html
in R0, the implication also has a special status, as in the implementation of
Rule R', explicit reference is made to the implication symbol (which replaces
the turnstile).
Hence both, HOL and R0, are identical in that there are three primitive
constants: equality (identity), epsilon/description operator, and implication.
4. "As primitive principles of definition and type definition, we use only the
core constant of equality, and so avoid any dependence on defined notions like
the existential quantifier." (p. 7)
Agreed. Peter B. Andrews: "Henkin's paper is of particular interest in that it
takes symbols for the identity relation as the sole primitive constants."
[Andrews, 1963, p. 345]
There is a recent historical note by Andrews ("A Bit of History Related to
Logic Based on Equality", 2014) at
http://dx.doi.org/10.1007/978-3-319-09719-0_8
not linked at his homepage currently, in which he describes the close
collaboration with Leon Henkin during that period, when Andrews was at
Princeton University (until finishing his Ph.D. there in 1964 with Alonzo
Church as advisor) and Henkin at the Institute for Advanced Study in Princeton
as how they "together [...] searched [Andrews'] card file of bibliographic
references" for some reference "in the logical literature to defining
quantifiers as well as propositional connectives in terms of equality" (p. 68).
5. From John Harrison, Josef Urban and Freek Wiedijk: History of Interactive
Theorem Proving
"Another limitation of the simple HOL type system is that there is no explicit
quantifier over polymorphic type variables, which can make many standard
results like completeness theorems and universal properties awkward to express,
though there are extensions with varying degrees of generality that fix this
issue [Melham, 1992; Voelker, 2007; Homeier, 2009]. Inflexibilities of these
kinds certainly arise in simple type theories, and it is not even clear that
more flexible dependent type theories (where types can be parametrized by
terms) are immune. For example, in one of the most impressive formalization
efforts to date [Gonthier et al., 2013] the entire group theory framework is
developed in terms of subsets of a single universe group, apparently to avoid
the complications from groups with general and possibly heterogeneous types."
http://www.cl.cam.ac.uk/~jrh13/papers/joerg.pdf (p. 36)
http://dx.doi.org/10.1016/B978-0-444-51624-4.50004-6
Group theory can be very naturally expressed with type abstraction, as done in
R0.
See the definition of groups ("Grp", p. 359) at
http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf
To keep formalization efforts low, I chose a simple example of a group in the
R0 implementation: (o, XOR).
First, I derived a simple property for all groups, the uniqueness of the
identity element ("GrpIdElUniq", p. 364).
Then it is shown that (o, XOR) is a group ("XorGroup", p. 416):
Grp o XOR
(Note that type 'o' - the type of truth values - appears as regular term here
suitable for lambda application including lambda-conversion/beta-reduction, as
with type abstraction, types are not a separate syntactic category anymore, but
terms of type tau - the type of types.)
Finally, the general theorem on the uniqueness of the identity element valid
for all groups can simply be instantiated for the specific example group (o,
XOR) without having to carry out the first proof again ("XorGrpIdElUniq",
p. 419).
This approach, taking advantage of a higher expressiveness with type
abstraction, is clearly more elegant than the current Isabelle/HOL language
extension (axiomatic type classes), which introduces something in between a
constant and a variable, allowing a constant to be declared first (line 1 of
example 2) and to be defined later (line 3) at:
http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-itp2015.pdf (p.
2)
http://dx.doi.org/10.1007/978-3-319-22102-1_16
This gives the "constant" the rights of a variable without imposing the
corresponding duties (restrictions), which Kuncar exploited to express a
classical paradox with the two characteristic properties: negativity (negation)
and self-reference (impredicativity). Kuncar and Popescu found a way to keep
track of the dependencies in order to avoid circularity, however, I would argue
that this is an auxiliary solution, as the dependencies should be recorded
explicitly with the syntactic means of the formal language (as intended by
Russell), which is the typing (allowing only certain wffs) and the restriction
on (type) variables in Rule R' in Q0/R0 or the binding of (type) variables with
lambda, respectively.
As mentioned off-list, a PDF version of "HOL Done Right" would be desirable
(and maybe long-term availability, e.g., via the UCAM-CL-TR series).
Best,
Ken
____________________
Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100
> Am 24.10.2016 um 04:55 schrieb john.harri...@cl.cam.ac.uk:
>
> Hi Ken,
>
> | 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 am glad you found it interesting. Indeed, I don't think I've ever
> written a detailed canonical description of the HOL Light foundations,
> though there are brief summaries scattered in various places, so this is
> certainly something to think about.
>
> On the history of HOL Light and related systems, in addition to those
> you have already discussed, let me shamelessly plug a book chapter
> written by Josef Urban, Freek Wiedijk and myself on the history of
> interactive theorem proving in general. This in particular discusses LCF
> and its successors, especially HOL, in section 3, complete with another
> little "family DAG" of HOL systems on page 19:
>
> http://www.cl.cam.ac.uk/~jrh13/papers/joerg.html
>
> Also of historical interest may be my old unpublished note "HOL Done
> Right":
>
> http://www.cl.cam.ac.uk/~jrh13/papers/holright.html
>
> That describes an intermediate stage in the evolution of HOL Light when
> the logical kernel still had implication as a primitive. The setup
> described there is also of some relevance to the discussion of type
> definition principles in a related thread, because it sketches what (as
> Rob notes in his paper) was the first version of a definitional
> principle that is roughly a "unary" version of his own idea. At the risk
> of reiterating what you can read in Rob's paper, let me explain my
> motivations there.
>
> Roger Jones gave an excellent description of the origins of what in
> HOL88 were called "new_definition" (a simple |- c = t binding) and
> "new_specification" (introducing constants satisfying a predicate given
> an existential theorem). One more perceived rough edge in HOL88 and
> hol90 that I wanted to fix in HOL Light was that there should indeed be
> two completely different definitional principles when they are
> tantalizingly close to being interderivable:
>
> * Since |- exists x. x = t is clearly provable, one can derive
> "new_definition" fron "new_specification". There is however a
> bootstrapping problem because "new_definition" is used to
> define the existential quantifier on which "new_specification"
> depends!
>
> * Once the epsilon operator is present, one can easily derive
> "new_specification" from "new_definition", but only with the
> motivating drawback mentioned by Roger Jones that you get
> "too much information" about the introduced constants.
>
> In the early versions of HOL Light I chose the slightly different
> approach of taking as primitive a variant of "new_specification" that
> allowed one to introduce a new constant c and a theorem |- P[c] given an
> input theorem |- P[t] for a specific term t, not |- exists x. P[x] as in
> "new_specification". Then no quantifiers are involved, and
> "new_definition" is a trivial instance because of reflexivity |- t = t,
> while "new_specification" can be derived from the epsilon operator
> without exposing too much information. One needs of course some
> restrictions on variables and type variables analogous to those Roger
> discussed. (Amusingly, I too got them wrong in the first instance, as
> Tom Melham spotted instantly when I first showed him the code. This
> was long before HOL Light was a public system.)
>
> At some point I switched HOL Light back to the simple |- c = t
> "new_definition" because it seemed slightly simpler and more intuitive,
> and I have personally never been very interested in the "too much
> information" problem (I generally want to define things explicitly, not
> leave them underspecificed). I can quite well see the arguments for
> Rob's version though.
>
> John.
------------------------------------------------------------------------------
Developer Access Program for Intel Xeon Phi Processors
Access to Intel Xeon Phi processor-based developer platforms.
With one year of Intel Parallel Studio XE.
Training and support from Colfax.
Order your platform today. http://sdm.link/xeonphi
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
