53 views

Skip to first unread message

May 11, 2017, 6:16:39 AM5/11/17

to p...@csl.sri.com, meta...@googlegroups.com, Prof. Peter B. Andrews

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' [lambda]-terms like \a. \x:a. 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 p{oa}e{a} is inferred [...] (which in set theory is expressed by e

∈ p) [...] 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

The SHA-512 checksum for file 'R0-v1.0.0.tar.gz' is:

538e742c5d42258cf460e46d84c60ceb fa6b5843efba4f73c2c17206f5bab931

7f6edb31686b933147abd17af8114277 b833baf189f42c2b7587c409aecaed1f

Kind regards,

Ken Kubota

____________________

Ken Kubota

http://doi.org/10.4444/100

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' [lambda]-terms like \a. \x:a. 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 p{oa}e{a} is inferred [...] (which in set theory is expressed by e

∈ p) [...] 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

The SHA-512 checksum for file 'R0-v1.0.0.tar.gz' is:

538e742c5d42258cf460e46d84c60ceb fa6b5843efba4f73c2c17206f5bab931

7f6edb31686b933147abd17af8114277 b833baf189f42c2b7587c409aecaed1f

Kind regards,

Ken Kubota

____________________

Ken Kubota

http://doi.org/10.4444/100

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu