[Hol-info] The definitional principles of HOL and equivalent mechanisms in Q0/R0

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

Hi John,

Thanks for the additional information. I will need some time to digest the 
papers you refer to.


Concerning the definitional principles of HOL, already in the past I have spent 
some thoughts about how to express the same in Q0/R0, and consider including 
some remarks in my R0 publication.

To avoid misunderstandings, let me refer to the extensions of the logic as 
discussed in sections 2.5.1 - 2.5.4 of the current HOL4 manual at:
	http://freefr.dl.sourceforge.net/project/hol/hol/kananaskis-10/kananaskis-10-logic.pdf


2.5.1 Extension by constant definition (John: "new_definition")

In the R0 implementation, definitions are not implemented as part of the 
logical kernel, but are labels attached to well-formed formulae (wffs) used for 
parsing and printing. I consider definitions simply as abbreviations, hence 
there is no need to make them part of the logical reasoning by introducing 
theorems for them. Consequently, definitions (abbreviations) can be removed and 
introduced again at any time without consequences for the reasoning itself, and 
without the danger of causing an inconsistency. (The wff to be abbreviated 
doesn't even need to be a closed term.) See the following R0 log, where 
comments start with (##) and output with (#):

## print universal quantifier ALL (A)
## (short and long - fully typed - version)
A
# wff      29 :  [\t.[\p.((=_[\x.T])_p)]]                   :=  A
# w typd   29 :  
[\t{^}{^}.[\p{{o,t{^}}}{{o,t{^}}}.((={{{o,{o,t{^}}},{o,t{^}}}}_[\x{t{^}}{t{^}}.T
{o}]{{o,t{^}}}){{o,{o,t{^}}}}_p{{o,t{^}}}{{o,t{^}}}){o}]{{o,{o,t{^}}}}]
## for the formatted version, see p. 356 at:
## http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf

## print Axiom 1 (Law of Excluded Middle) - with defined ALL
%A1
#                ((=_((&_(g_T))_(g_F)))_((A_o)_[\x.(g_x)]))
[...]
## for the formatted version, see p. 351 at:
## http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf
## or Andrews' version for Q0 at:
## http://plato.stanford.edu/entries/type-theory-church/#ForBasEqu

## remove definition of universal quantifier ALL (A)
:= A

## print Axiom 1 (Law of Excluded Middle) - without defined ALL
%A1
#                ((=_((&_(g_T))_(g_F)))_(([\t.[\p.((=_[\x.T])_p)]]_o)_[\x.(g_x)]))
[...]

## define universal quantifier again (with type information)
:= A [\t{^}{^}.[\p{{o,t{^}}}{{o,t{^}}}.((={{{o,{o,t{^}}},{o,t{^}}}}_[\x{t{^}}{t{^}}.T
{o}]{{o,t{^}}}){{o,{o,t{^}}}}_p{{o,t{^}}}{{o,t{^}}}){o}]{{o,{o,t{^}}}}]
# wff      29 :  [\t.[\p.((=_[\x.T])_p)]]                   :=  A

## print Axiom 1 (Law of Excluded Middle) - with defined ALL again
## there is no difference to the original result above
%A1
#                ((=_((&_(g_T))_(g_F)))_((A_o)_[\x.(g_x)]))
[...]

## remove all definitions used in Axiom 1
:= &; := T; := F; := A

## print Axiom 1 (Law of Excluded Middle) - without any definition, as it is 
actually in the logic
## consisting only of the constant equality (=), variables, lambda abstraction 
(\), and application (_)
%A1
#                
((=_(([\x.[\y.((=_[\g.((g_((=_=)_=))_((=_=)_=))])_[\g.((g_x)_y)])]]_(g_((=_=)_=)
))_(g_((=_[\x.((=_=)_=)])_[\x.x]))))_(([\t.[\p.((=_[\x.((=_=)_=)])_p)]]_o)_[\x.(
g_x)]))


2.5.2 Extension by constant specification (John: "new_specification")

The specification example in the manual
	¬(b1 = b2)
or
	not (b1 = b2)
with b1 and b2 of type bool could be introduced as a hypothesis h.

Then we would have theorems
	h |- t1
	h |- t2
etc.

If h would be inconsistent (h |- F), we could prove: not h.

Otherwise (the consistent case), the variables (b1 and b2) in h are free, e.g.,
	not (b1 = b2) |- t1
	not (b1 = b2) |- t2
such that the restrictions on free variables in the set of hypotheses for Rule 
R' [Andrews, 2002, p. 214] apply, and hence, the "variables" practically behave 
like constants, as in HOL. Note that neither the Rule of Universal 
Generalization (5220) nor the Rule of Substitution (5221) are applicable due to 
their restrictions on free variables in the set of hypotheses [cf. Andrews, 
2002, p. 222], which means that b1 and b2 could not be instantiated if they 
would appear as free variables in t1 or t2.


2.5.3 Remarks about constants in HOL

This passage, according to my memory the same as the original by Andy Pitts, 
discusses the "dependency on type variables", arguing that "explicitly 
recording dependency of constants on type variables makes for a rather 
cumbersome syntax".
However, with type abstraction, types are not a separate syntactic category 
anymore, but terms of type tau. This means that the type variables are subject 
to the same restrictions of Rule R' as regular variables, resulting in a 
uniform treatment of both regular and type variables, and in addition to that, 
the binding of type variables with lambda preserves dependency information.
With the means of type abstraction, explicit tracking of the dependency on type 
variables can be expressed very naturally with the means of the formal 
language, as (in general) intended by Russell.


2.5.4 Extension by type definition

The corresponding mechanism in R0 was described recently:

"In R0, the interpretation of types is that of (nonempty) sets. Naturally, one 
would see, for example,
the number 3 as a natural number, and therefore has its type:
	3 : N   (or "3_N" in Tex/LaTeX notation)
[...]
The consequence is, of course, that a mathematical entity may have several 
types, as naturally
one would like to express 3 : N, 3 : S5, or 3 : R (three is a real number).
[...]
Since terms like [\x.x<5] (S5, the set of the numbers smaller than 5), can 
become a type, the strict
distinction between terms and types is removed, as when a theorem like
	(S5 3)
is obtained, S5 becomes a type by adding the types of types (tau) to it, and
to the number 3 the new type S5 is added."
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-October/msg00050.html

The advantage in comparison to the HOL mechanism is, as I believe, that new 
types are introduced very naturally, no axioms have to be assumed, and there 
is no duplication of mathematical structures (linked with a bijection / an 
isomorphism).


In summary, the definitional principles of HOL can be equivalently expressed by
- allowing wffs to be printed (and parsed) by shorthands attached to them,
- Andrews' Rule R' (with a uniform treatment of regular variables and type 
variables),
- and a simple, natural mechanism for introducing new types.
Forgive me if I made a mistake while quickly writing down my ideas.


Concerning HOL Light, I recall that in the current R0 draft (from May 18, 
2015), HOL Light is the main reference, as it has the same underlying concept 
of an extremely small logical kernel:
"The axioms of R0 are only logical axioms. For a number of reasons discussed 
below no non-logical axioms (those not necessary for formal logic) are allowed 
in R0. HOL Light has 'three mathematical axioms' [Harrison, 2009, p. 62], and 
two of them are non-logical axioms: the axiom of choice and the axiom of 
infinity.
In summary, if 'HOL Light is [...] a clean and simplified version of Mike 
Gordon's original HOL system' [Harrison, 2009, p. 60], then R0 is even cleaner 
and simpler than HOL Light and follows consequently the path of maximising 
logical rigor by reductionism." [Kubota, 2015, p. 14 f.]
(Maybe the comparison is slightly unfair, since R0 is not designed for 
automation, opting for Hilbert-style like Q0.)

Also, other design decisions for HOL Light and R0 are identical.
For example, having to decide between variable names and a numbering system for 
variables (like de Bruijn indices), I opted for names in order to make the 
logical reasoning as explicit as possible (besides better readability).
Similarly, you wrote on HOL Light: "I reimplemented all the prelogic 
completely, abandoning de Bruijn terms in favour of a return to name-carrying 
syntax."
	https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf (p. 222)


Maybe it is best to continue discussion after the publication of R0, when 
comparisons can be made easier.


Best,

Ken

____________________

Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100



P.S.:

The full internal representation of Axiom 1 (Law of Excluded Middle), which is 
exposed if all definitions (abbreviations) are removed, is - without and with 
full type information -:

%A1
#                
((=_(([\x.[\y.((=_[\g.((g_((=_=)_=))_((=_=)_=))])_[\g.((g_x)_y)])]]_(g_((=_=)_=)
))_(g_((=_[\x.((=_=)_=)])_[\x.x]))))_(([\t.[\p.((=_[\x.((=_=)_=)])_p)]]_o)_[\x.(
g_x)]))
#                                                           :=  A1
#                
((={{{o,o},o}}_(([\x{o}{o}.[\y{o}{o}.((={{{o,@},@}}_[\g{{{o,o},o}}{{{o,o},o}}.((
g{{{o,o},o}}{{{o,o},o}}_((={{{o,@},@}}_={@}){{o,@}}_={@}){o}){{o,o}}_((={{{o,@},
@}}_={@}){{o,@}}_={@}){o}){o}]{@}){{o,@}}_[\g{{{o,o},o}}{{{o,o},o}}.((g{{{o,o},o
}}{{{o,o},o}}_x{o}{o}){{o,o}}_y{o}{o}){o}]{@}){o}]{{o,o}}]{{{o,o},o}}_(g{{o,o}}{
{o,o}}_((={{{o,@},@}}_={@}){{o,@}}_={@}){o}){o}){{o,o}}_(g{{o,o}}{{o,o}}_((={{{o
,{o,o}},{o,o}}}_[\x{o}{o}.((={{{o,@},@}}_={@}){{o,@}}_={@}){o}]{{o,o}}){{o,{o,o}
}}_[\x{o}{o}.x{o}{o}]{{o,o}}){o}){o}){o}){{o,o}}_(([\t{^}{^}.[\p{{o,t{^}}}{{o,t{
^}}}.((={{{o,{o,t{^}}},{o,t{^}}}}_[\x{t{^}}{t{^}}.((={{{o,@},@}}_={@}){{o,@}}_={
@}){o}]{{o,t{^}}}){{o,{o,t{^}}}}_p{{o,t{^}}}{{o,t{^}}}){o}]{{o,{o,t{^}}}}]{{{o,{
o,\3{^}}},^}}_o{^}){{o,{o,o}}}_[\x{o}{o}.(g{{o,o}}{{o,o}}_x{o}{o}){o}]{{o,o}}){o
})



> 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.