[isabelle] Publication of the Mathematical Logic R0: Mathematical Formulae

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

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. 

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


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)

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