[Hol-info] Type quantifiers, definability of logical constants/quantifiers/connectives, equality, group theory (expressiveness with type abstraction)

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

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