[isabelle] Practical considerations (automation) vs. "pure" logic (expressiveness/reducibility)



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.