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