Dear List Members,
dear Norman Megill,
As a contribution to the recent discussion which started in February at
https://groups.google.com/d/msg/metamath/DRMh8ZPA6Mo/BtCdxJ9FDgAJ
please allow me to forward my announcement attached below.
Metamath is very similar to Q0, as it tries to formalize mathematics with
a minimal set of symbols and rules:
"Unlike most other systems, Metamath attempts to use the minimum
possible framework needed to express mathematics and its proofs."
http://us.metamath.org/index.html
Q0 has only a "single rule of inference", and it "requires only two basic
types (individuals and truth values) and only two basic constants
(identity/equality and its counterpart, description)".
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html
For a short description of Q0, please see
https://plato.stanford.edu/entries/type-theory-church/#ForBasEqu
Hence the claim of uniqueness isn't valid anymore, as Metamath's
"philosophy of simplicity" does not only hold for the logic Q0 (described in
literature), too, but also for the further development R0, which is (like HOL)
both a logic and a software implementation:
"Metamath is unique in this sense, offering an alternative approach for those
attracted to its philosophy of simplicity."
http://us.metamath.org/index.html
I would argue that Q0 is even more consequent than Metamath, as
Metamath's "philosophy of simplicity", which corresponds to
Andrews' concept of expressiveness (I also use the term
reducibility), is realized in the specification of the formal language, too,
specifically by the virtues of lambda notation, such that Schönfinkel's
idea of reducing functions to functions of one argument can
be expressed very naturally.
As I haven't heard anything different after my first message on this list,
I have attributed the quotes to Norman Megill, see pp. 8 f. at
http://www.owlofminerva.net/files/fom.pdf
Kind regards,
Ken Kubota
____________________
Ken Kubota
http://doi.org/10.4444/100
> Anfang der weitergeleiteten Nachricht:
>
> Von: Ken Kubota <
ma...@kenkubota.de>
> Betreff: Publication of the Mathematical Logic R0: Mathematical Formulae
> Datum: 10. April 2017 um 12:17:57 MESZ
> An: HOL-info list <
hol-...@lists.sourceforge.net>,
cl-isabe...@lists.cam.ac.uk,
coq-...@inria.fr
> Kopie: "Prof. Peter B. Andrews" <
and...@cmu.edu>, "Prof. Michael J. C. Gordon" <
mj...@cl.cam.ac.uk>, "Prof. Thomas F. Melham" <
thomas...@balliol.ox.ac.uk>, "Prof. Andrew M. Pitts" <
Andrew...@cl.cam.ac.uk>, John Harrison <
John.H...@cl.cam.ac.uk>
>
> Dear Members of the Research Community,
>
> I am pleased to announce the publication of the mathematical logic R0, a
> further development of Peter B. Andrews' logic Q0. The syntactic features
> provided by R0 are type variables (polymorphic type theory), the binding of
> type variables with the abstraction operator and single variable binder λ (type
> abstraction), and (some of) the means necessary for dependent types (dependent
> type theory).
>
> The publication is available online at
>
http://www.owlofminerva.net/files/formulae.pdf
>
> The introduction can be found on pp. 11 f.
>
> A printed copy can be ordered with ISBN 978-3-943334-07-4. The software
> implementation is expected to be published in due course. For more information,
> please visit:
http://doi.org/10.4444/100.3
>
>
> The expressiveness of the formal language obtained with type abstraction allows
> for a natural formulation of group theory [cf. p. 12 of
>
http://www.owlofminerva.net/files/formulae.pdf ]. With the set (type) of Boolean
> values o, the exclusive disjunction XOR, and an appropriate definition of
> groups Grp [p. 362], the fact that (o, XOR) is a group can be expressed in
> lambda notation with [p. 420]
> Grp o XOR
>
> This enhancement of the expressiveness of the formal language overcomes the
> "limitation of the simple HOL type system [...] that there is no explicit
> quantifier over polymorphic type variables, which can make many standard
> results [...] awkward to express [...]. [...] For example, in one of the most
> impressive formalization efforts to date [Gonthier et al., 2013] the entire
> group theory framework is developed in terms of subsets of a single universe
> group, apparently to avoid the complications from groups with general and
> possibly heterogeneous types." [Harrison, Urban, and Wiedijk, 2014, pp. 170 f.]
>
> Furthermore, the enhanced expressiveness provided by R0 avoids the
> circumlocutions connected with preliminary solutions like axiomatic type
> classes recently developed and discussed for Isabelle/HOL. The expressiveness
> of type abstraction also replaces the notion of compound types, which in HOL
> are used for ordered pairs (the Cartesian product, see section 1.2 of
>
http://freefr.dl.sourceforge.net/project/hol/hol/kananaskis-11/kananaskis-11-logic.pdf ),
> that in R0 can be formalized without compound types [cf. pp. 378 f. of
>
http://www.owlofminerva.net/files/formulae.pdf ].
>
>
> Mike Gordon's HOL developed at Cambridge University is, like Andrews' logic Q0,
> based on the Simple Theory of Types (1940) developed by Alonzo Church, Andrews'
> Ph.D. advisor at Princeton University. Among the HOL group, there has always
> been the awareness that besides automation, there is the philosophical
> (logical) desire to reduce the means of the logic to a few principles. In the
> HOL handbook, Andrew M. Pitts wrote the legendary sentence: "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 and Melham, 1993, p. 213]
>
> In the same spirit, Mike Gordon wrote on the genesis of HOL: "[T]he terms [...]
> could be encoded [...] in such a way that the LSM expansion-law just becomes a
> derived rule [...]. This approach is both more elegant and rests on a firmer
> logical foundation, so I switched to it and HOL was born." [Gordon, 2000, p.
> 173]
>
> The general principle of reducing the logic (including the language) to a few
> principles is the main criterion for the design of Q0 (having only a single
> primitive rule of inference, Rule R), which is summarized by Peter B. Andrews
> as follows: "Therefore we shall turn our attention to finding a formulation of
> type theory which is as expressive as possible, allowing mathematical ideas to
> be expressed precisely with a minimum of circumlocutions, and which is as
> simple and economical as is possible without sacrificing expressiveness. The
> reader will observe that the formal language we find arises very naturally from
> a few fundamental design decisions." [Andrews, 2002, pp. 205 f.]
>
> R0 "follows Andrews' concept of expressiveness (I also use the term
> reducibility), which aims at the ideal and natural language of formal logic and
> mathematics.“ [p. 11 of
http://www.owlofminerva.net/files/formulae.pdf ]
>
>
> Like John Harrison's HOL Light, R0 has an extremely small kernel. R0 resembles
> Norman Megill's Metamath, which "attempts to use the minimum possible framework
> needed to express mathematics and its proofs.“ (
http://us.metamath.org/ ) For
> the same reason, R0 is, unlike most other systems, a Hilbert-style system.
>
> R0 uses, like Q0, the description operator, avoiding the problems of the
> epsilon operator already discussed by Mike Gordon himself for HOL: "It must be
> admitted that the ε-operator looks rather suspicious." [Gordon, 2001, p. 24]
> "The inclusion of ε-terms into HOL 'builds in' the Axiom of Choice [...]."
> [Gordon, 2001, p. 24]
>
> Unlike in Coq, in R0, the Curry-Howard isomorphism is not used, favoring a
> direct (unencoded) expression rather than the encoding of proofs. For the same
> reason, it is an object logic and not a logical framework (such as Larry
> Paulson's Isabelle and Norman Megill's Metamath). Like Cris Perdue’s Prooftoys
> (
http://prooftoys.org ,
http://mathtoys.org ) - a natural deduction variant of
> Andrews' Q0 - in R0, the turnstile symbol is replaced by the logical
> implication [p. 12].
>
>
> Kind regards,
>
> Ken Kubota
>
> ____________________
>
> Ken Kubota
>
http://doi.org/10.4444/100
>
>
> References
>
> Kubota, Ken (2017), Mathematical Formulae. Available online at
>
http://www.owlofminerva.net/files/formulae.pdf (April 9, 2017). SHA-512:
> 2ca7be176113ddd687ad8f7ef07b6152 770327ea7993423271b84e399fe8b507
> 67a071408594ec6a40159e14c85b97d2 168462157b22017d701e5c87141157d8. ISBN:
> 978-3-943334-07-4. DOI: 10.4444/100.3. See:
http://doi.org/10.4444/100.3
>
>
> For further references, please see
>
http://www.owlofminerva.net/files/fom.pdf (direct link)
>
http://doi.org/10.4444/100.111 (persistent link)
>