*To*: cl-isabelle-users at lists.cam.ac.uk, hol-info at lists.sourceforge.net*Subject*: [isabelle] Literature on the type system of Isabelle/HOL; HOL documentation; non-logical axioms vs. definitions; epsilon vs. description operator (HOL vs. Q0); Rule R of Andrews' logic Q0*From*: Ken Kubota <mail at kenkubota.de>*Date*: Mon, 15 Aug 2016 17:36:22 +0200*Cc*: "Prof. Lawrence C. Paulson" <lp15 at cam.ac.uk>, "Prof. Michael J. C. Gordon" <mjcg at cl.cam.ac.uk>, "Prof. Thomas Melham" <thomas.melham at balliol.ox.ac.uk>, "Prof. Peter B. Andrews" <andrews at cmu.edu>*In-reply-to*: <66DB665D-1072-4029-8AD5-F4FB0EAABCD4@cam.ac.uk>*References*: <2D14D352-3D4D-4FDE-ABA4-0168BF6E04F3@kenkubota.de> <5F22105EAD3CAD4689EC4570AA1802B0BF0197C539@WGFP-EXMAV1.uni.mdx.ac.uk> <A6A56921-0B58-4CF4-9786-DBF6E77F286C@kenkubota.de> <1468731439.2162406.668416497.16BBD60D@webmail.messagingengine.com> <25BFF9C0-748B-49E0-9C6F-3E799076E217@kenkubota.de> <66DB665D-1072-4029-8AD5-F4FB0EAABCD4@cam.ac.uk>

Dear Members of the Research Community, Please allow me to add a few comments. 1. First, I would like to thank Larry Paulson for providing the download link for Mike Gordon's text at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00047.html answering my inquiry at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00046.html What Gordon calls "'second order' [lambda]-terms like \a. \x:a. x, [which] perhaps [...] should be included in the HOL logic" at http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.6103&rep=rep1&type=pdf (p. 22) is implemented in R0 as the main feature of dependent type theory (i.e., the binding of type variables with lambda) and called "type abstraction" there: http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (pp. 356 ff.) It might be worth considering publishing this 2001 version of Gordon's paper within the technical report series in order to ensure long-term (online) availability of the currently only cached document. In addition, online availability of the 1985 version (UCAM-CL-TR-68) is desirable, as it is still of historical interest. Also, I would like to thank Tom Melham for bringing to my attention his approach of implementing in the HOL logic the idea of explicit quantification over type variables as presented by Andrews in 1965: "I have found Andrews' book [1] invaluable in working out many of the technical details of the extension to HOL proposed here." http://www.cs.ox.ac.uk/tom.melham/pub/Melham-1994-HLE.pdf (p. 15) I have addressed this issue and discussed details in my draft: "It has to be noted that already in his PhD thesis 'A Transfinite Type Theory with Type Variables' published in 1965 Andrews is very near to developing a dependent type theory. [...] In the system Q with type variables the universal quantifier (â) becomes a true variable binder in the case of types, but in the case of terms (objects) a definition depending on Î." [Kubota, 2015, p. 31] However, for some reason Andrews refrained from directly using lambda as type variable binder, which would exhibit the reducibility of the variable binders to a single one, as was done in R0. 2. In the LOGIC part of the documentation of the current HOL system, reference is made to Rule R of Andrews' logic 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." http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf (p. 27) Is it possible to figure out the author of this sentence? I am considering quoting it and would like to credit authorship in such a case. 3. Preferring definitions over the use of non-logical axioms as discussed at https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00046.html has a major advantage to be mentioned. If the conditions are not introduced as axioms, but as properties within the definition, and these conditions later turn out to be contradictory, they do not render the system inconsistent as a whole, but only demonstrate that no mathematical object ("model") can satisfy these conditions, which is formally expressed by the emptiness of the defined set, which is the desired result (in the simplest case concerning the types, i.e., a unary predicate; otherwise tuples may be used). For this reason, and for other reasons, such as not constraining expressiveness of the system, instead of postulating a (non-logical) Axiom of Infinity (usually over the type of individuals), the Peano axioms should be part of the definition of natural numbers (which can be expressed without axioms quite simply and naturally in dependent type theory), that guarantees the set to be infinite: "Actually, any set satisfying postulates P1-P4 must be infinite." [Andrews, 2002, p. 259] Then there is no need to add an Axiom of Infinity as Axiom 6, which extends Q0 to Q0^inf [cf. Andrews, 2002, p. 259]. For the same reasons, the use of language elements which make implicit use of axioms should be avoided. Gordon correctly states: "The inclusion of [epsilon]-terms into HOL 'builds in' the Axiom of Choice [...]." Somewhat earlier on the same page, he quite frankly confesses: "It must be admitted that the [epsilon]-operator looks rather suspicious." http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.6103&rep=rep1&type=pdf (p. 24) Implicit use of the Axiom of Choice can be avoided by using the description operator instead, like in Q0 and R0, where it is the counterpart to identity (equality) [cf. Andrews, 2002, pp. 211, 213; Kubota, 2015]. For example, the "conditional term Cond t t_1 t_2 (meaning 'if t then t_1 else t_2')" "defined using the [epsilon]-operator" at http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.6103&rep=rep1&type=pdf (p. 24) can be defined using the description operator [cf. Andrews, 2002, pp. 235 f. (5313)]; software verification of the formal proof has been provided in [Kubota, 2015, pp. 165-174]. The (verification of the) formal proof and the axioms for R0 have now been made available online at: http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf Please note that in Axiom 5 (Axiom of Descriptions) and throughout the whole system the primitive symbol for identity (equality) 'Q' used in Q0 [cf. Andrews, 2002, pp. 211, 213] was eliminated and replaced by the identity symbol '=' in R0, as the symbol 'Q' syntactically doesn't have an own independent function: http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf (pp. 351 f.) It then becomes even more obvious that description is the counterpart to identity, extracting the single element from a singleton (unit set), and eliminating the identity symbol '='. 4. Rule R is indeed presented by Andrews as the "single rule of inference" [Andrews, 2002, p. 213] of Q0. However, already on the following page, a variant, Rule R', is specified [cf. p. 214], which also takes into account a set of hypotheses. Hence, logically, one might regard Rule R' as the general rule and Rule R only as the special case in which the set of hypotheses is empty. Technically, both Rule R and Rule R' are implemented in the dependent type theory R0 as two different routines due to the access to different parts of the formulae, but both routines then use the same subroutine. Rule R and Rule R' are called Âs and Âs' in R0, where the section sign (Â) indicates a rule, and 's' stands for substitution: http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (pp. 362 f.) Rule Â\ ('\' stands for lambda) denotes lambda-conversion (or more specifically, beta-conversion), which in Andrews' Q0 is obtained as theorem 5207 [cf. Andrews, 2002, p. 218 f.] from Axiom Schemata 4_1 - 4_5. Since some of the Axiom Schemata 4_1 - 4_5 contain restrictions, lambda-conversion was implemented as a rule in R0. As the active elements, rules may contain restrictions, but not theorems (including axioms/axiom schemata), which are passive elements. This alternative method of implementing lambda-conversion was already considered by Andrews in a paragraph to which he directed my attention when I met him and which is already contained in the first edition (1986): "5207 could be taken as an axiom schema in place of 4_1 - 4_5, and for some purposes this would be desirable, since 5207 has a conceptual simplicity and unity which is not apparent in 4_1 - 4_5." [Andrews, 1986, p. 165; Andrews, 2002, p. 214] The fact that lambda-conversion is actually a process (i.e., active, dynamic, and hence, a rule), and not only a (passive, static) theorem, axiom, or axiom schema, becomes obvious in the online presentation of Q0, where Axiom Schemata 4_1 - 4_5 are replaced by 5207 as new Axiom Schema 4 which makes use of a function "SubFree" denoting the process of substitution (of all free occurrences of a variable): http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/#ForBasEqu Similarly, in Church's simple theory of types, lambda-conversion (beta-conversion) is implemented as the second (beta-reduction, also called beta-contraction) and third (beta-expansion) of altogether six rules of inference [cf. Church, 1940, p. 60]. Kind regards, Ken Kubota References Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Orlando: Academic Press. ISBN 0-12-058535-9 (Hardcover). ISBN 0-12-058536-7 (Paperback). Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: 10.1007/978-94-015-9934-4. Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia of Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/ (July 2, 2016). Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In: Journal of Symbolic Logic 5, pp. 56-68. Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18, 2015). Unpublished manuscript. SHA-512: a0dfe205eb1a2cb29efaa579d68fa2e5 45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50 011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See: http://dx.doi.org/10.4444/100.10 Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (p. 1, pp. 356-364, pp. 411-420, and pp. 754-755). Available online at http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf (January 24, 2016). SHA-512: 67a48ee12a61583bd82c286136459c0c 9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783 3d1047d1831bc357eb57b263b44c885b. Kubota, Ken (2015b), Excerpt from [Kubota, 2015] (p. 1, pp. 165-174, and pp. 350-352). Available online at http://www.kenkubota.de/files/R0_draft_excerpt_with_axioms_and_proof_of_C_function.pdf (August 13, 2016). SHA-512: 8702d932d50f2e1f6b592dc03b6f283e 64ba18f881150b4ae32e4b915249d241 3db34ba4c3dcf0e0cdef25b679d9615f 424adb1803a179e578087ded31b573b9. ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100

**References**:**[isabelle] Literature on the type system of Isabelle/HOL; text by Mike Gordon***From:*Ken Kubota

**Re: [isabelle] Literature on the type system of Isabelle/HOL; text by Mike Gordon***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Question about numerals
- Next by Date: [isabelle] AFP statistics
- Previous by Thread: Re: [isabelle] Literature on the type system of Isabelle/HOL; text by Mike Gordon
- Next by Thread: [isabelle] New in the AFP: The Imperative Refinement Framework
- Cl-isabelle-users August 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