*To*: "Dr. Markus Wenzel" <makarius at sketis.net>*Subject*: [isabelle] Practical considerations (automation) vs. "pure" logic (expressiveness/reducibility)*From*: Ken Kubota <mail at kenkubota.de>*Date*: Fri, 2 Sep 2016 17:19:41 +0200*Cc*: OndÅej KunÄar <kuncar at in.tum.de>, "Prof. Andrew M. Pitts" <Andrew.Pitts at cl.cam.ac.uk>, cl-isabelle-users at lists.cam.ac.uk, "Prof. Lawrence C. Paulson" <lp15 at cam.ac.uk>, "Prof. Peter B. Andrews" <andrews at cmu.edu>, Andrei Popescu <a.popescu at mdx.ac.uk>, hol-info at lists.sourceforge.net*In-reply-to*: <9754103c-82f6-77b9-29e9-8a62ac31fbcd@sketis.net>*References*: <CDD6C40D-96BE-46B5-99F1-C9C35A8CE6D6@kenkubota.de> <AM3PR01MB1313544EEAE1E863CEF17D97B7E90@AM3PR01MB1313.eurprd01.prod.exchangelabs.com> <0192D3B0-CE89-40F5-A978-629B40D5E207@kenkubota.de> <5bfdc080-bf44-a033-9827-6d8c3b7fef05@in.tum.de> <827BA885-4683-457C-B89C-F264921E267C@kenkubota.de> <9754103c-82f6-77b9-29e9-8a62ac31fbcd@sketis.net>

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

- Previous by Date: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Next by Date: Re: [isabelle] Telling auto to use an eisbach method
- Previous by Thread: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Next by Thread: [isabelle] Reconciling FinFuns in Distro and AFP
- Cl-isabelle-users September 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list