*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Implementing the higher-order logic Q0 within the Isabelle proof assistant software*From*: Ken Kubota <mail at kenkubota.de>*Date*: Mon, 27 Jul 2015 20:45:58 +0200*Cc*: "Prof. Lawrence C. Paulson" <lp15 at cam.ac.uk>, "Prof. Peter B. Andrews" <andrews at cmu.edu>

Dear Members of the Research Community, For the purpose of implementing Peter B. Andrews' logic Q0 as presented in his standard work on higher-order logic titled "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof" within the Isabelle proof assistant software, I am looking for experts who are familiar with Isabelle and who would be interested in this project. The higher-order logic Q0 has an extremely high level of formalization/mechanization (the rules applied in each single step are explicitly specified [cf. Andrews, 2002, pp. 215 ff.]), and virtually all of mathematics is reduced to formal logic according to Russell's and Whitehead's idea of logicism. The universality of Q0 as a foundation of mathematics is preserved by its independence of philosophical assumptions such as the semantic approach of model theory, as the single rule of inference (substitution, from which the rule of modus ponens is derived) is a purely syntactical rule. Technically, Q0 is typed lambda calculus in the form of a simple type theory (i.e., without type variables) and an axiomatic (Hilbert-style) deductive system with identity (equality) as the main notion, hence an improved formulation of Church's type theory [Church, 1940; cf. Andrews, 2006], which is known for its "precise formulation of the syntax" [Paulson, 1989, p. 5]. Featuring lambda calculus with the single variable binder lambda and "only four separate kinds of primitive terms: variables, constants, function applications and [lambda]-abstractions" [Gordon, 2000, p. 179], Q0 requires only two basic types (individuals and truth values) and only two basic constants (identity/equality and its counterpart, description) in order to obtain definability of all of the propositional connectives, as well as all of the quantifiers (universal, existential and uniqueness quantifier) and provability of elementary logic on the basis of only five logical axioms, and formalized number theory (with a non-logical axiom of infinity), thus reducing the language of formal logic and mathematics to a minimal set of basic notions. The general intent is to obtain a system with the highest level of formalization and accuracy and with the expressiveness required for formalization (of most or all) of mathematics such that the mathematician, logician or philosopher can easily work with it whilst avoiding the burden of technical details (i.e., software configuration or programming languages) without compromising logical necessity or otherwise weakening logical rigor. The implementation of Q0 should be exactly as specified in [Andrews, 2002, pp. 210-215] (as a Hilbert-style system). A short description is available online at [Andrews, 2006]: http://plato.stanford.edu/entries/type-theory-church/#ForBasEqu According to a recent e-mail by Lawrence C. Paulson, an implementation of Q0 as a Hilbert-style system (as a special case within natural deduction) in Isabelle should be possible. The paper "A Formulation of the Simple Theory of Types (for Isabelle)" by Paulson, in which Q0 is mentioned ("Andrews [1] presents a formulation based on equality." [Paulson, 1989, p. 14]) and in which simple type theory is implemented, but as a natural deduction system, may serve as a basis. If you would like to find out more about this project, please contact me via my website (see below). Ken Kubota References 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. (2006), "Church's Type Theory". In: Stanford Encyclopedia of Philosophy. Ed. by Edward N. Zalta. Available online at http://plato.stanford.edu/entries/type-theory-church/ (July 25, 2015). Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In: Journal of Symbolic Logic 5, pp. 56-68. Gordon, Mike (2000), "From LCF to HOL: A Short History". In: Proof, Language, and Interaction. Ed. by Gordon Plotkin, Colin Stirling, and Mads Tofte. Cambridge, MA et al.: MIT Press, pp. 169-185. Paulson, Lawrence C. (1989), "A Formulation of the Simple Theory of Types (for Isabelle)". Available online at https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-175.pdf (July 25, 2015). ____________________ Ken Kubota doi: 10.4444/100 http://dx.doi.org/10.4444/100

**Follow-Ups**:

- Previous by Date: [isabelle] New AFP category "Tools"
- Next by Date: [isabelle] Contracting Abbreviations of Locale Definitions
- Previous by Thread: [isabelle] New AFP category "Tools"
- Next by Thread: Re: [isabelle] Implementing the higher-order logic Q0 within the Isabelle proof assistant software
- Cl-isabelle-users July 2015 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