Ken Kubota

An Owl of Minerva Press site

Author: Ken Kubota

Software Implementation of the Mathematical Logic R0 Available for Download

Dear Members of the Research Community,

I am pleased to announce that the software implementation of the mathematical logic R0, a further development of Peter B. Andrews’ logic Q0, is now available. 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 software implementation can be downloaded (license restrictions apply) at
http://doi.org/10.4444/100.10.3

 

The logic R0 does not only allow quantification over types with quantifiers, as specified in [Andrews, 1965] and [Melham, 1993b], but, moreover, the binding of type variables with lambda (type abstraction), as suggested by Mike Gordon for HOL:

“[…] ‘second order’ λ-terms like λ𝛼. λx:𝛼. x, perhaps such terms should be included in the HOL logic.” [Gordon, 2001, p. 22]

The expressiveness of the formal language obtained with type abstraction allows for a natural formulation of group theory [cf. p. 12 of http://doi.org/10.4444/100.10.2]. 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.]

While in both Andrews’ Q0 and Gordon’s HOL the universal quantifier is defined as

ALL  :=  [\p. p = [\x.T] ]

[Andrews, 2002, p. 212; Gordon and Melham, 1993], in R0, with type abstraction, the type is made explicit:

ALL  :=  [\t. [\p. p = [\x.T] ] ]

with p of type (ot), or t -> o [p. 359 of http://doi.org/10.4444/100.10.2].

Then, the set-theoretic proposition

ALL n : NAT . n+1 > 0

in type theory can be expressed very naturally by

ALL NAT [\n . n+1 > 0]

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, cf. [Gordon and Melham, 1993]), that in R0 can be formalized without compound types [cf. pp. 378 f. of http://doi.org/10.4444/100.10.2].

 

R0 has an intuitive method of type introduction, which does not require the additional axioms of the HOL type introduction mechanism: “Whenever a theorem of the form po𝛼e𝛼 is inferred […] (which in set theory is expressed by ep) […] p is acknowledged as a type” [p. 11 of http://doi.org/10.4444/100.10.2].

 

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://doi.org/10.4444/100.10.2] Therefore R0 is, unlike most other implementations, a Hilbert-style system, opting for expressiveness instead of automation.

R0 implements the philosophical program of Russell’s and Whitehead’s Principia Mathematica, logicism, i.e., the reduction of mathematics to formal logic, and even more, generalizes this idea by reducing formal logic itself to a few principles.

 

Like John Harrison’s HOL Light, R0 has an extremely small logical kernel. Being a Hilbert-style system, it has the smallest number of rules of inference among the programs implementing a fixed logic (not regarding logical frameworks with another kind of expressiveness). 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/]

With a size of less than 100 KB, it is the smallest proof checker or interactive theorem prover, including the current versions of John Harrison’s HOL Light, Mark Adams’ HOL Zero, Norman Megill’s Metamath, and Freek Wiedijk’s reimplementation of Automath.

Like Q0, R0 uses the description operator, avoiding the problems of the epsilon operator for HOL already discussed by Mike Gordon himself:

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

R0 and PVS are the only implementations based on classical type theory with some form of dependent types. Also, R0 and PVS are the only implementations based on classical type theory with mathematical entities that may have different types (or which have at least some form of subtyping).

Unlike in Coq, in R0, no use is made of the Curry-Howard isomorphism, favoring a direct (unencoded, and hence, natural) expression rather than the encoding of proofs. For the same reason, it is an object (fixed) logic and not a logical framework (such as Larry Paulson’s Isabelle and Norman Megill’s Metamath). Like in 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 of http://doi.org/10.4444/100.10.2].

R0 is, together with HOL Zero [Adams, 2016, p. 34], the only proof checker or interactive theorem prover which has the property of Pollack-consistency, namely

“being able to correctly parse formulas that it printed itself” [Wiedijk, 2012, p. 85].

R0 is the only proof checker or interactive theorem prover which can correctly parse whole proofs (and not only formulas) that it printed itself. Finally, R0 has the property of

faithfulness, where internal representation and concrete syntax correctly correspond. A printer that printed false as true and true as false might be Pollack-consistent but would not be faithful.” [Adams, 2016, p. 21]

R0 is, like Automath, a mere proof checker (practically without any automation at all).

 

A full treatment of R0 shall be announced at
http://doi.org/10.4444/100.10.1

For references, please see: http://doi.org/10.4444/100.111

 

Kind regards,

Ken Kubota

____________________

Ken Kubota
http://doi.org/10.4444/100

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

Recommendations on Mathematical Scientific Literature

From time to time, I receive requests from mathematicians for recommendations on scientific literature. My recommendation is always chapter 5 of Andrews’ 2002 textbook, in which the higher-order logic Q0 is presented [Andrews, 2002, pp. 210–215], and elementary logic developed (e.g., the derivation of the rule of Modus Ponens [p. 224]). For the full reference, please see the overview.

Further Resources

Photograph with Peter B. Andrews, the Creator of the Logic Q0

Professor Peter B. Andrews and Ken Kubota (2010)
Foto Copyright © 2017 Ken Kubota

The picture above with Peter B. Andrews and me was made on January 14, 2010, at Carnegie Mellon University in Pittsburgh, Pennsylvania (USA). It is published first here in 2017.

Professor Andrews is the creator of the higher-order logic Q0, the leading mathematical system in terms of elegance and expressiveness among the logistic systems publicly available as of today. Formal logic and most of mathematics can be expressed in it in a very natural way, on the basis of two primitive symbols only (identity/equality and its counterpart, description).

Andrews’ type theory Q0 is further developed in my still unpublished logic and software implementation R0, which has type variables and type abstraction allowing for dependent types. (Some excerpts are available online.)

For an overview about logics including Q0 and R0, please see the Foundations of Mathematics (Genealogy and Overview).

I would like to thank Peter for his kind permission to place the picture on my homepage.

Further Resources

© 2017 Ken Kubota

Theme by Anders NorenUp ↑