Re: [isabelle] Implementing the higher-order logic Q0 within the Isabelle proof assistant software



Please forgive me because I have not fully understood the motivations
behind this project, and I do not want to criticise it unfairly. But I do
want to make an observation.

As I understand it, Q0 is in some sense equivalent to the "HOL" that is
already formalised in Isabelle (i.e., Isabelle/HOL), and almost all of the
virtues of Q0 mentioned in your email apply also to that formalisation.
Indeed there already exists substantial formalisations of mathematics and
computer science in Isabelle/HOL.

Furthermore, there are already several variations of theorem provers
implementing a roughly equivalent logic. The ones I can name off the top of
my head include: Isabelle/HOL, HOL4, HOL Light, ProofPower/HOL, HOL Zero,
and Mosquito. The OpenTheory project could be considered another variation,
or as a step towards unification: it defines a standard library and an
interface format aimed at sharing formal developments between all these
variations of HOL.

There may be very good reasons to implement Q0 following Andrews's
original, historical and elegant, approach. But if there happen not to be
any motivations beyond increasing the proliferation of implementations of
HOL, I would be wary of doing it.

On 27 July 2015 at 19:45, Ken Kubota <mail at kenkubota.de> wrote:

> 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
>
>
>



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