Dear Makarius Wenzel,
dear Members of the Research Community,
The "tradeoff" argument concerning the "tradeoff in theoretical simplicity
versus complexity required for practical applications of logic" given at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00084.html
reminds me of an e-mail discussion I had with Larry Paulson about natural
deduction vs. axiomatic (Hilbert-style) deductive systems (with respect to
automation). Of course, certain concessions cannot be avoided, and for
automation, natural deduction (making metatheorems symbolically representable)
is the only choice, although one would like to prefer a Hilbert-style system in
which all rules of inference can be reduced to a single one, like in Q0.
Nevertheless, one has to be aware that concessions for practical reasons (e.g.,
automation) are deviations from the "pure" logic, and while deviations
concerning certain decisions are necessary, for all other decisions, the
original concept remains, and the general design decisions still apply.
In the HOL handbook, this is reflected by Andrew Pitts' consideration regarding
Q0:
"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]
https://sourceforge.net/p/hol/mailman/message/35287517/
What Andrews calls "expressiveness" [Andrews, 2002, p. 205], is what I, vice
versa, call "reducibility", and this concept is already implicit in Church's
work (the simple theory of types), in which reducibility is omnipresent either
as Currying (reducing functions of more than one argument to functions with
only one argument, due to Schoenfinkel, implemented via lambda-conversion) or
as the definability of the logical connectives (reducing them to combinations
of a small set of primitive symbols).
Moreover, reducibility (expressiveness) is not just "theoretical simplicity".
The reduction of symbols, variable binders, axioms, and rules of inference lays
bare the inner logic of formal logic and mathematics, and reveals
interdependencies between them. This holds for both interdependencies within
each field (e.g., for rules: between primitive and derived rules, for symbols:
between primitive and defined symbols, etc.) as well as interdependencies among
the fields (e.g., the derivability of the rule of modus ponens from a certain
set of rules and axioms). (Also independence: In Andrews' Q0, it is shown that
elementary logic is independent of the Axiom of Choice, which is, in my
opinion, a non-logical axiom, like the Axiom of Infinity. In Gordon's HOL, this
is not possible, since the use of the epsilon operator instead of the
description operator makes the Axiom of Choice inevitable.) Exactly this
- laying bare the inner logic of formal logic and mathematics - makes Church's
and Andrews' formulations of the mathematical language so important, not only
Church's (and Andrews') "precise formulation of the syntax"
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-175.pdf (p. 5),
which also is the result of consequently carrying out the principle of
reducibility (expressiveness). Church's main achievement is the creation of a
mathematical language largely following the concept of
expressiveness/reducibility; whereas this concept seems to be implicit in the
work of Church, it is explicit in the work of Andrews.
Hence, while practical considerations enforce deviations from the "pure" logic,
still implementations (e.g., Gordon's HOL or Isabelle/HOL) are based on and
have to face comparison with the "pure" logical system (e.g., Q0).
Therefore practical concessions are in some sense a layer on top of (or,
"overloading") the "pure" logic in certain areas, but do not render the general
concept of expressiveness (reducibility) irrelevant. So it is not simply an
alternative between logical rigor and practical considerations, but the latter
overrides the general concept in certain fields only. It is important to keep
this root (i.e., the underlying, but partially covered concept) and its
remaining validity in mind (e.g., the reducibility not of rules, but still of
symbols, variable binders, and axioms; avoidance of the use of the Axiom of
Choice by preferring the description operator to the epsilon operator). With
the above quote from the documentation of the original (Gordon's) HOL system,
this awareness is clearly expressed.
Concerning "type class instantiation", my guess is that with dependent type
theory, the more expressive mathematical language provides other means which
might replace the features provided by the current Isabelle/HOL (polymorphic
type theory). At least certain language features of the original (Gordon's) HOL
system, such as
a) the introduction (definition) of types [cf. Gordon/Melham, 1993, pp. 225
ff.; cf. paragraph 2.5.4 of
http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf
(pp. 38 ff.) ],
b) or the use of compound types [cf. Gordon/Melham, 1993, p. 195; cf. paragraph
1.2 of
http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf
(p. 11)]
can be expressed very naturally in the dependent type theory R0, and from its
point of view, these HOL language features then appear as rather artificial
extensions (even with the introduction of new axioms!) which were necessary to
emulate some of the expressiveness of the language of dependent type theory
with the limited means of the language of polymorphic type theory, and, hence,
as a preliminary and auxiliary solution.
Regarding the concerns about expanding abbreviations (definitions), this kind
of argument is not applicable to all representations of logic. In the R0
implementation, formulae are represented as binary trees, each having assigned
a natural number. So internally, any well-formed formula (wff) can be addressed
by its number, and expansion (and definition) is only a question of parsing and
printing, but not of the logical core (in which no definitions exist, but only
binary trees and their numbers representing expanded wffs). Of course, due to
Isabelle's concept of a meta-logical framework, or other practical
considerations, different circumstances may be relevant that I am not familiar
with.
For the HOL documentation team, it might be worth considering making the
brilliant HOL documents, such as
http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf
available directly on the HOL homepage in order to make it readable within the
browser, e.g., via
https://hol-theorem-prover.org/documents/kananaskis-10-logic.pdf
since a download is a barrier for many people, for example, due to security
considerations, or at public terminals providing browsing, but not downloading.
For references, please see:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00069.html
https://sourceforge.net/p/hol/mailman/message/35287517/
Kind regards,
Ken Kubota
____________________
Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
