121 views

Skip to first unread message

Apr 15, 2017, 6:40:44 AM4/15/17

to meta...@googlegroups.com, Norman Megill, Prof. Peter B. Andrews

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)

>

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)

>

Apr 15, 2017, 8:54:24 AM4/15/17

to Metamath, n...@alum.mit.edu, and...@cmu.edu, ma...@kenkubota.de

I'm an amateur and not pursuing that career thing, so I have a different perspective. From what I've seen, this field is driven mostly by its applications. And a rich type systems have a more natural appeal for software verification than a small kernel systems. Of course, these have their merit too, otherwise we wouldn't be here, right? What attracts me is that common philosophical views on their subject. But their community interests look very specific and could be qualified more like a theoretical toy. As I've seen myself, professional mathematicians are not interested in foundations of mathematics as a tool of their everyday work. It'd require Newton or Einstein to actually make something great out of it. I'd like to know how others perceive it and if they actually wish to share their views?

Apr 15, 2017, 4:00:55 PM4/15/17

to meta...@googlegroups.com, Norman Megill, Prof. Peter B. Andrews

The phrase "small kernel" refers to a _small logical kernel_ separable

from the rest of the software implementation, and the property of

having such a logical kernel sometimes is referred to as

"LCF approach" or "de Bruijn criterion":

"The de Bruijn criterion states that the correctness of the mathematics

in the system should be guaranteed by a small checker. Architecturally

this generally means that there is a ‘proof kernel’ that all the mathematics

is filtered through."

http://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf (p. 10)

With this approach, the correctness of the inferences depends on the

kernel only, which allows extensions and modifications of the software

without any effect on the correctness (as long as the modifications

were made outside of the kernel).

So the LCF approach is a matter of the architectural design of the software,

but does not confine the logic to having either a poor or rich type system.

Both Metamath (according to the reference above) and R0 have such

a small logical kernel.

Many professional mathematicians specialize on certain subjects,

but of course there are (professional) mathematicians and computer

scientists who are interested in the foundations of mathematics,

among them are Andrews, Megill, Harrison, and Wiedijk.

Clearly, Andrews' Q0 is designed to be a (type theoretic) logic and

foundation for expressing mathematics, and (set theoretic) Metamath

apparently has the same objective.

For an overview on current systems, I would recommend the papers

[Wiedijk, 2003] and [Wiedijk, 2007] referenced in section 1 of

http://www.owlofminerva.net/files/fom.pdf

There are some general reflections in [Andrews, 2002].

I plan to write a text explaining the philosophical foundations of R0,

but there is little chance that it will be published before next year.

It will be announced or linked at

http://doi.org/10.4444/100.10

from the rest of the software implementation, and the property of

having such a logical kernel sometimes is referred to as

"LCF approach" or "de Bruijn criterion":

"The de Bruijn criterion states that the correctness of the mathematics

in the system should be guaranteed by a small checker. Architecturally

this generally means that there is a ‘proof kernel’ that all the mathematics

is filtered through."

http://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf (p. 10)

With this approach, the correctness of the inferences depends on the

kernel only, which allows extensions and modifications of the software

without any effect on the correctness (as long as the modifications

were made outside of the kernel).

So the LCF approach is a matter of the architectural design of the software,

but does not confine the logic to having either a poor or rich type system.

Both Metamath (according to the reference above) and R0 have such

a small logical kernel.

Many professional mathematicians specialize on certain subjects,

but of course there are (professional) mathematicians and computer

scientists who are interested in the foundations of mathematics,

among them are Andrews, Megill, Harrison, and Wiedijk.

Clearly, Andrews' Q0 is designed to be a (type theoretic) logic and

foundation for expressing mathematics, and (set theoretic) Metamath

apparently has the same objective.

For an overview on current systems, I would recommend the papers

[Wiedijk, 2003] and [Wiedijk, 2007] referenced in section 1 of

http://www.owlofminerva.net/files/fom.pdf

There are some general reflections in [Andrews, 2002].

I plan to write a text explaining the philosophical foundations of R0,

but there is little chance that it will be published before next year.

It will be announced or linked at

http://doi.org/10.4444/100.10

Apr 15, 2017, 4:53:31 PM4/15/17

to Metamath, n...@alum.mit.edu, and...@cmu.edu, ma...@kenkubota.de

Thanks for your answer.

On Saturday, April 15, 2017 at 11:00:55 PM UTC+3, Ken Kubota wrote:

So the LCF approach is a matter of the architectural design of the software,

but does not confine the logic to having either a poor or rich type system.

Yes, but the software implementations surely have some design preferences which could make it better fit for certain applications. Seems that the current trend is to prefer complex software systems for computer science problems, while it's more viable to use simpler ones for the work related to foundations of mathematics. And I have an impression that most practical effort goes into computer science applications, which could be seen by a number of implementations alone.

Many professional mathematicians specialize on certain subjects,

but of course there are (professional) mathematicians and computer

scientists who are interested in the foundations of mathematics,

among them are Andrews, Megill, Harrison, and Wiedijk.

True. I was wondering how your work is perceived as a directed effort toward some common goal perhaps, by a larger community.

I plan to write a text explaining the philosophical foundations of R0,

Thanks. That's what a most interesting part might look like from a point of view of a non-logician.

Apr 15, 2017, 6:19:36 PM4/15/17

to meta...@googlegroups.com, Norman Megill, Prof. Peter B. Andrews, Cris Perdue

> Am 15.04.2017 um 22:53 schrieb vvs <vvs...@gmail.com>:

>

> Thanks for your answer.

>

> On Saturday, April 15, 2017 at 11:00:55 PM UTC+3, Ken Kubota wrote:

> So the LCF approach is a matter of the architectural design of the software,

> but does not confine the logic to having either a poor or rich type system.

>

> Yes, but the software implementations surely have some design preferences which could make it better fit for certain applications. Seems that the current trend is to prefer complex software systems for computer science problems, while it's more viable to use simpler ones for the work related to foundations of mathematics. And I have an impression that most practical effort goes into computer science applications, which could be seen by a number of implementations alone.

From my experience, I would basically agree, but add some detail.
>

> Thanks for your answer.

>

> On Saturday, April 15, 2017 at 11:00:55 PM UTC+3, Ken Kubota wrote:

> So the LCF approach is a matter of the architectural design of the software,

> but does not confine the logic to having either a poor or rich type system.

>

> Yes, but the software implementations surely have some design preferences which could make it better fit for certain applications. Seems that the current trend is to prefer complex software systems for computer science problems, while it's more viable to use simpler ones for the work related to foundations of mathematics. And I have an impression that most practical effort goes into computer science applications, which could be seen by a number of implementations alone.

The complex software systems are very good in finding (automating)

mathematical proofs, but automating proofs is, which supports your statement,

not related to the foundations of mathematics.

Without judging the philosophical concept, but looking at the

technical software design only, there are, roughly spoken,

three levels of (software) complexity:

1. simple software implementations: Automath, Metamath, R0

2. medium complex software implementations: HOL, HOL Light, HOL Zero

3. very complex software implementations: Isabelle [Isabelle/HOL]

The simple software implementations, providing little or no automation,

are rather proof checkers and are suited for mathematics only.

The medium and complex software implementations are used for

both mathematics and practical applications such as hardware verification.

But from the philosophical point of view, the simple software implementations

have the most sophisticated philosophical ideas behind them and are

better suited for the foundation of mathematics.

Another clear distinction is Hilbert-style vs. natural deduction.

For automation, natural deduction is inevitable.

If you look at the diagram on p. 1 of

http://www.owlofminerva.net/files/fom.pdf

you will see Q0 and HOL as the two descendants of Church's STT.

Q0 is the more philosophical system with its focus on expressiveness

(hence, Hilbert-style), whereas HOL is designed for automation

necessary for practical applications (hence, natural deduction).

I am not sure whether Metamath is Hilbert-style or natural deduction,

and already had a short discussion with Cris Perdue about this.

It might even be a third alternative, since Metamath is a logical framework.

The reason why I do not consider Metamath as fully Hilbert-style is, that,

being a logical framework, it has some meta-level (or meta-theory),

rendering, at the very first glance, the Metamath substitution rule

practically a representation of many rules expressed in a different manner.

In the design of (Hilbert-style) R0, it was important for me that there

is no meta-theory at all, which is also the reason why the turnstile is

replaced by the logical implication (a decision that was made

independently by Cris Perdue, too, for his Prooftoys system, a

natural deduction variant of Q0).

> Many professional mathematicians specialize on certain subjects,

> but of course there are (professional) mathematicians and computer

> scientists who are interested in the foundations of mathematics,

> among them are Andrews, Megill, Harrison, and Wiedijk.

>

> True. I was wondering how your work is perceived as a directed effort toward some common goal perhaps, by a larger community.

so I do not expect a very quick scientific resonance.

But, of course, with R0 I share and implement Russell's philosophical

concept of logicism (reducing mathematics to formal logic),

and some other philosophical ideas.

The exact opposite is Larry Paulson's Isabelle with its focus

on automation. Similar to the the pocket calculator, which automated

numerical calculations, Isabelle might be the future tool which

automates proofs.

R0 is not designed as a technical tool, but is, like Metamath,

inspired by Whitehead and Russell's Principia Mathematica,

trying to find the foundation of mathematics in the form of "the

ideal and natural language of formal logic and mathematics".

http://www.owlofminerva.net/files/formulae.pdf (p. 11)
Apr 15, 2017, 7:56:11 PM4/15/17

to metamath

Hi Ken,

I've been interested in the discussions surrounding this new logic / software system, but frankly I don't know how to enter the arena because it hasn't been made clear to me what R0 *is*, as a logic. Your publication is over 800 pages of computer output, with only one page on motivation and no "how to read this paper" discussion. What does the program do, and how? Given where you are publishing I already know it is a proof verifier for a new logic, but the nature of this logic is not clear, and without this I cannot effectively perform a comparison with Metamath.On Sat, Apr 15, 2017 at 6:19 PM, Ken Kubota <ma...@kenkubota.de> wrote:

> Am 15.04.2017 um 22:53 schrieb vvs <vvs...@gmail.com>:

>

> Thanks for your answer.

>

> On Saturday, April 15, 2017 at 11:00:55 PM UTC+3, Ken Kubota wrote:

> So the LCF approach is a matter of the architectural design of the software,

> but does not confine the logic to having either a poor or rich type system.

>

> Yes, but the software implementations surely have some design preferences which could make it better fit for certain applications. Seems that the current trend is to prefer complex software systems for computer science problems, while it's more viable to use simpler ones for the work related to foundations of mathematics. And I have an impression that most practical effort goes into computer science applications, which could be seen by a number of implementations alone.

From my experience, I would basically agree, but add some detail.

The complex software systems are very good in finding (automating)

mathematical proofs, but automating proofs is, which supports your statement,

not related to the foundations of mathematics.

Without judging the philosophical concept, but looking at the

technical software design only, there are, roughly spoken,

three levels of (software) complexity:

1. simple software implementations: Automath, Metamath, R0

2. medium complex software implementations: HOL, HOL Light, HOL Zero

3. very complex software implementations: Isabelle [Isabelle/HOL]

The simple software implementations, providing little or no automation,

are rather proof checkers and are suited for mathematics only.

The medium and complex software implementations are used for

both mathematics and practical applications such as hardware verification.

I want to remind you that the link between a kernel and an interface with automation need not be one-to-one. In particular, Metamath can be small and still have automation of arbitrary complexity. This is similar to the LCF kernel approach, except this suggests the image that the kernel is one part of a single behemoth program, where I prefer to think of one (or more) kernels extended with additional automation packages or IDEs in a pluralistic way

As such, I reject the above inference that Metamath and similar systems cannot be used for hardware verification because they lack automation capabilities, since this can be added after the fact. You can have your cake and eat it too in this way.

Another clear distinction is Hilbert-style vs. natural deduction.

For automation, natural deduction is inevitable.

If you look at the diagram on p. 1 of

http://www.owlofminerva.net/files/fom.pdf

you will see Q0 and HOL as the two descendants of Church's STT.

Q0 is the more philosophical system with its focus on expressiveness

(hence, Hilbert-style), whereas HOL is designed for automation

necessary for practical applications (hence, natural deduction).

I am not sure whether Metamath is Hilbert-style or natural deduction,

and already had a short discussion with Cris Perdue about this.

It might even be a third alternative, since Metamath is a logical framework.

The reason why I do not consider Metamath as fully Hilbert-style is, that,

being a logical framework, it has some meta-level (or meta-theory),

rendering, at the very first glance, the Metamath substitution rule

practically a representation of many rules expressed in a different manner.

I need not point out that Metamath clearly brands itself as a Hilbert-style system. If you take pure Metamath, with no axioms, the "one axiom" involves substitution into theorems, applied as inference rules. This gives proofs a clear tree (or dag) structure, and is not significantly different from either Hilbert-style or natural deduction (written as tree proofs of Gamma |- phi, not trees of formulas with hypothesis cancellation).

In the design of (Hilbert-style) R0, it was important for me that there

is no meta-theory at all, which is also the reason why the turnstile is

replaced by the logical implication (a decision that was made

independently by Cris Perdue, too, for his Prooftoys system, a

natural deduction variant of Q0).

This distinction makes no sense to me. What does the head symbol have to do with it? Do you have a complete and unambiguous specification of R0's logical system that I could look at?

Mario Carneiro

Apr 16, 2017, 7:49:11 AM4/16/17

to Metamath

воскресенье, 16 апреля 2017 г., 2:56:11 UTC+3 пользователь Mario Carneiro написал:

As such, I reject the above inference that Metamath and similar systems cannot be used for hardware verification because they lack automation capabilities, since this can be added after the fact. You can have your cake and eat it too in this way.

That's a very interesting statement, especially considering that it's coming from you. Do you have a specific plans for Metamath in this regard? When I asked about "a larger community" I expected to hear some philosophical and even practical goals. It's very frustrating that no clear direction is drawn by this community. Where is Metamath going and who is directing it there? Well, I don't expect something similar to Hilbert's program, but some clarification would be nice. I understand that it's mostly a hobby project, but I believe it deserves a better role. Are you aware of Univalent foundations initiative? Could something similar be born from Metamath enthusiasts?

Apr 16, 2017, 10:47:34 AM4/16/17

to meta...@googlegroups.com, HOL-info list, Prof. Peter B. Andrews

Hi Mario,

Since some of the questions (no. 2) are relevant for type theory, too,

let me copy to the HOL list, and answer below each quoted passage.

The whole discussion can be found at

https://groups.google.com/forum/#!topic/metamath/s19SSncdtiM

> Am 16.04.2017 um 01:56 schrieb Mario Carneiro <di....@gmail.com>:

>

> Hi Ken,

>

> I've been interested in the discussions surrounding this new logic / software system, but frankly I don't know how to enter the arena because it hasn't been made clear to me what R0 *is*, as a logic. Your publication is over 800 pages of computer output, with only one page on motivation and no "how to read this paper" discussion. What does the program do, and how? Given where you are publishing I already know it is a proof verifier for a new logic, but the nature of this logic is not clear, and without this I cannot effectively perform a comparison with Metamath.

1.

R0 is based on and very similar to Q0, so studying Peter B. Andrews' Q0

is the first step.

The reference is [Andrews, 2002, pp. 201–237] as specified on p. 11 of

http://www.owlofminerva.net/files/formulae.pdf

A large portion of the proofs formalized in my publication is directly

taken from there, e.g., the derivation of Modus Ponens, for which

the source is given (p. 94):

"Source: [Andrews 2002 (ISBN 1-4020-0763-9), p. 224]"

The proofs in Andrews' 2002 textbook are much more reader friendly.

R0 extends Q0 with type variables and binding of type variables with

lambda (type abstraction), which allows for explicit quantification over

types as desired by John Harrison at el. for HOL in the paper quoted.

Peter is Professor Emeritus at CMU and still living in Pittsburgh,

according to his email from last month. As you seem to be a

Ph.D. student at CMU, you might have the chance to meet him

and ask questions about Q0.

My publication is only one of three parts, as indicated at

http://doi.org/10.4444/100.10

I will try to make the software available as soon as possible.

The text with the full explanation might be published next year.

I will send you the 2015 draft for private use.

Please do not quote without explicit permission.

The R0 implementation allows to express all wffs of R0 and

obtain all inferences of R0 using the rules mentioned on p. 12.

R0 takes commands from a file or interactively, and only

mathematically valid theorems can be obtained.

The input and source code files are in subsections 2.2.*,

and the formatted output files are in subsections 2.1.*.

Hence the R0 software represents the R0 logic, and ideally,

this should be more or less identical with mathematics in general.

(more below)

> On Sat, Apr 15, 2017 at 6:19 PM, Ken Kubota <ma...@kenkubota.de> wrote:

> > Am 15.04.2017 um 22:53 schrieb vvs <vvs...@gmail.com>:

> >

> > Thanks for your answer.

> >

> > On Saturday, April 15, 2017 at 11:00:55 PM UTC+3, Ken Kubota wrote:

> > So the LCF approach is a matter of the architectural design of the software,

> > but does not confine the logic to having either a poor or rich type system.

> >

> > Yes, but the software implementations surely have some design preferences which could make it better fit for certain applications. Seems that the current trend is to prefer complex software systems for computer science problems, while it's more viable to use simpler ones for the work related to foundations of mathematics. And I have an impression that most practical effort goes into computer science applications, which could be seen by a number of implementations alone.

>

> From my experience, I would basically agree, but add some detail.

> The complex software systems are very good in finding (automating)

> mathematical proofs, but automating proofs is, which supports your statement,

> not related to the foundations of mathematics.

>

> Without judging the philosophical concept, but looking at the

> technical software design only, there are, roughly spoken,

> three levels of (software) complexity:

>

> 1. simple software implementations: Automath, Metamath, R0

> 2. medium complex software implementations: HOL, HOL Light, HOL Zero

> 3. very complex software implementations: Isabelle [Isabelle/HOL]

>

> The simple software implementations, providing little or no automation,

> are rather proof checkers and are suited for mathematics only.

> The medium and complex software implementations are used for

> both mathematics and practical applications such as hardware verification.

>

> I want to remind you that the link between a kernel and an interface with automation need not be one-to-one. In particular, Metamath can be small and still have automation of arbitrary complexity. This is similar to the LCF kernel approach, except this suggests the image that the kernel is one part of a single behemoth program, where I prefer to think of one (or more) kernels extended with additional automation packages or IDEs in a pluralistic way

>

> As such, I reject the above inference that Metamath and similar systems cannot be used for hardware verification because they lack automation capabilities, since this can be added after the fact. You can have your cake and eat it too in this way.

2.

I'm not familiar with Metamath in detail, and might be mistaken

and apologize for this.

Of course, ZFC is a very expressive, but for general reasons,

I consider type theory the better approach for expressing

mathematics than (axiomatic) set theory.

Type theory prevents the paradoxes by means of the language,

as it makes the classification of mathematical objects explicit.

The concept of (axiomatic) set theory then appears as a rather

auxiliary solution, since with the distinction between classes and

sets first all inferences are forbidden, and with the axioms some

are allowed again. This renders the set of axioms as historically

arbitrary (the mathematics currently used), as shown with later

additions like axioms for large cardinals.

So (axiomatic) set theory does not provide a systematic solution

like type theory, which uses the means of the formal language

for preventing the paradoxes as intended by Russell.

> Another clear distinction is Hilbert-style vs. natural deduction.

> For automation, natural deduction is inevitable.

> If you look at the diagram on p. 1 of

> http://www.owlofminerva.net/files/fom.pdf

> you will see Q0 and HOL as the two descendants of Church's STT.

> Q0 is the more philosophical system with its focus on expressiveness

> (hence, Hilbert-style), whereas HOL is designed for automation

> necessary for practical applications (hence, natural deduction).

>

> I am not sure whether Metamath is Hilbert-style or natural deduction,

> and already had a short discussion with Cris Perdue about this.

> It might even be a third alternative, since Metamath is a logical framework.

> The reason why I do not consider Metamath as fully Hilbert-style is, that,

> being a logical framework, it has some meta-level (or meta-theory),

> rendering, at the very first glance, the Metamath substitution rule

> practically a representation of many rules expressed in a different manner.

>

> I need not point out that Metamath clearly brands itself as a Hilbert-style system. If you take pure Metamath, with no axioms, the "one axiom" involves substitution into theorems, applied as inference rules. This gives proofs a clear tree (or dag) structure, and is not significantly different from either Hilbert-style or natural deduction (written as tree proofs of Gamma |- phi, not trees of formulas with hypothesis cancellation).

I would have to take a closer look at Metamath, but my main point will follow below.

> In the design of (Hilbert-style) R0, it was important for me that there

> is no meta-theory at all, which is also the reason why the turnstile is

> replaced by the logical implication (a decision that was made

> independently by Cris Perdue, too, for his Prooftoys system, a

> natural deduction variant of Q0).

>

> This distinction makes no sense to me. What does the head symbol have to do with it? Do you have a complete and unambiguous specification of R0's logical system that I could look at?

3.

[Andrews, 2002, pp. 201–237] together with my 2015 draft emailed to you

should be sufficient for a specification of the R0 logic.

The axioms for R0 can be found on pp. 353 ff. of

http://www.owlofminerva.net/files/formulae.pdf

For the definitions, see pp. 359 ff.

One approach is the semantic approach (model theory), which is

appealing to many mathematicians, as the justification for the syntactic

inference is expressed with mathematical means.

But there is also another possibility, the syntactic approach.

In philosophy, a justification by a meta-theory (in which the

semantic evaluation takes place in model theory) is considered

problematic.

If a theory is justified by a meta-theory, than what justifies the meta-theory?

Such an approach would be considered as "outward" in philosophy.

The alternative is trying to express as much as possible within (!) the language,

this approach is called "immanent" (= within).

For this reason, the meta-perspective (bird's view from top) as used

with the turnstile symbol for provability should not be used for

expressing rules: "The turnstile (⊢) was eliminated and replaced by

the logical implication (⊃) [e.g., cf. pp. 303 ff. (K8025 = Deduction Theorem)

and Andrews, 2002, pp. 228 f. (5240 = Deduction Theorem)]."

http://www.owlofminerva.net/files/formulae.pdf (p. 12)

The turnstile may be used for metamathematics expressing properties

of a formal system after (!) setting up the language and logic, but should

not be used before, legitimizing or setting up the logic itself.

> Mario Carneiro

Kind regards,

Ken Kubota

Since some of the questions (no. 2) are relevant for type theory, too,

let me copy to the HOL list, and answer below each quoted passage.

The whole discussion can be found at

https://groups.google.com/forum/#!topic/metamath/s19SSncdtiM

> Am 16.04.2017 um 01:56 schrieb Mario Carneiro <di....@gmail.com>:

>

> Hi Ken,

>

> I've been interested in the discussions surrounding this new logic / software system, but frankly I don't know how to enter the arena because it hasn't been made clear to me what R0 *is*, as a logic. Your publication is over 800 pages of computer output, with only one page on motivation and no "how to read this paper" discussion. What does the program do, and how? Given where you are publishing I already know it is a proof verifier for a new logic, but the nature of this logic is not clear, and without this I cannot effectively perform a comparison with Metamath.

R0 is based on and very similar to Q0, so studying Peter B. Andrews' Q0

is the first step.

The reference is [Andrews, 2002, pp. 201–237] as specified on p. 11 of

http://www.owlofminerva.net/files/formulae.pdf

A large portion of the proofs formalized in my publication is directly

taken from there, e.g., the derivation of Modus Ponens, for which

the source is given (p. 94):

"Source: [Andrews 2002 (ISBN 1-4020-0763-9), p. 224]"

The proofs in Andrews' 2002 textbook are much more reader friendly.

R0 extends Q0 with type variables and binding of type variables with

lambda (type abstraction), which allows for explicit quantification over

types as desired by John Harrison at el. for HOL in the paper quoted.

Peter is Professor Emeritus at CMU and still living in Pittsburgh,

according to his email from last month. As you seem to be a

Ph.D. student at CMU, you might have the chance to meet him

and ask questions about Q0.

My publication is only one of three parts, as indicated at

http://doi.org/10.4444/100.10

I will try to make the software available as soon as possible.

The text with the full explanation might be published next year.

I will send you the 2015 draft for private use.

Please do not quote without explicit permission.

The R0 implementation allows to express all wffs of R0 and

obtain all inferences of R0 using the rules mentioned on p. 12.

R0 takes commands from a file or interactively, and only

mathematically valid theorems can be obtained.

The input and source code files are in subsections 2.2.*,

and the formatted output files are in subsections 2.1.*.

Hence the R0 software represents the R0 logic, and ideally,

this should be more or less identical with mathematics in general.

(more below)

> On Sat, Apr 15, 2017 at 6:19 PM, Ken Kubota <ma...@kenkubota.de> wrote:

> > Am 15.04.2017 um 22:53 schrieb vvs <vvs...@gmail.com>:

> >

> > Thanks for your answer.

> >

> > On Saturday, April 15, 2017 at 11:00:55 PM UTC+3, Ken Kubota wrote:

> > So the LCF approach is a matter of the architectural design of the software,

> > but does not confine the logic to having either a poor or rich type system.

> >

> > Yes, but the software implementations surely have some design preferences which could make it better fit for certain applications. Seems that the current trend is to prefer complex software systems for computer science problems, while it's more viable to use simpler ones for the work related to foundations of mathematics. And I have an impression that most practical effort goes into computer science applications, which could be seen by a number of implementations alone.

>

> From my experience, I would basically agree, but add some detail.

> The complex software systems are very good in finding (automating)

> mathematical proofs, but automating proofs is, which supports your statement,

> not related to the foundations of mathematics.

>

> Without judging the philosophical concept, but looking at the

> technical software design only, there are, roughly spoken,

> three levels of (software) complexity:

>

> 1. simple software implementations: Automath, Metamath, R0

> 2. medium complex software implementations: HOL, HOL Light, HOL Zero

> 3. very complex software implementations: Isabelle [Isabelle/HOL]

>

> The simple software implementations, providing little or no automation,

> are rather proof checkers and are suited for mathematics only.

> The medium and complex software implementations are used for

> both mathematics and practical applications such as hardware verification.

>

> I want to remind you that the link between a kernel and an interface with automation need not be one-to-one. In particular, Metamath can be small and still have automation of arbitrary complexity. This is similar to the LCF kernel approach, except this suggests the image that the kernel is one part of a single behemoth program, where I prefer to think of one (or more) kernels extended with additional automation packages or IDEs in a pluralistic way

>

> As such, I reject the above inference that Metamath and similar systems cannot be used for hardware verification because they lack automation capabilities, since this can be added after the fact. You can have your cake and eat it too in this way.

I'm not familiar with Metamath in detail, and might be mistaken

and apologize for this.

Of course, ZFC is a very expressive, but for general reasons,

I consider type theory the better approach for expressing

mathematics than (axiomatic) set theory.

Type theory prevents the paradoxes by means of the language,

as it makes the classification of mathematical objects explicit.

The concept of (axiomatic) set theory then appears as a rather

auxiliary solution, since with the distinction between classes and

sets first all inferences are forbidden, and with the axioms some

are allowed again. This renders the set of axioms as historically

arbitrary (the mathematics currently used), as shown with later

additions like axioms for large cardinals.

So (axiomatic) set theory does not provide a systematic solution

like type theory, which uses the means of the formal language

for preventing the paradoxes as intended by Russell.

> Another clear distinction is Hilbert-style vs. natural deduction.

> For automation, natural deduction is inevitable.

> If you look at the diagram on p. 1 of

> http://www.owlofminerva.net/files/fom.pdf

> you will see Q0 and HOL as the two descendants of Church's STT.

> Q0 is the more philosophical system with its focus on expressiveness

> (hence, Hilbert-style), whereas HOL is designed for automation

> necessary for practical applications (hence, natural deduction).

>

> I am not sure whether Metamath is Hilbert-style or natural deduction,

> and already had a short discussion with Cris Perdue about this.

> It might even be a third alternative, since Metamath is a logical framework.

> The reason why I do not consider Metamath as fully Hilbert-style is, that,

> being a logical framework, it has some meta-level (or meta-theory),

> rendering, at the very first glance, the Metamath substitution rule

> practically a representation of many rules expressed in a different manner.

>

> I need not point out that Metamath clearly brands itself as a Hilbert-style system. If you take pure Metamath, with no axioms, the "one axiom" involves substitution into theorems, applied as inference rules. This gives proofs a clear tree (or dag) structure, and is not significantly different from either Hilbert-style or natural deduction (written as tree proofs of Gamma |- phi, not trees of formulas with hypothesis cancellation).

> In the design of (Hilbert-style) R0, it was important for me that there

> is no meta-theory at all, which is also the reason why the turnstile is

> replaced by the logical implication (a decision that was made

> independently by Cris Perdue, too, for his Prooftoys system, a

> natural deduction variant of Q0).

>

> This distinction makes no sense to me. What does the head symbol have to do with it? Do you have a complete and unambiguous specification of R0's logical system that I could look at?

[Andrews, 2002, pp. 201–237] together with my 2015 draft emailed to you

should be sufficient for a specification of the R0 logic.

The axioms for R0 can be found on pp. 353 ff. of

http://www.owlofminerva.net/files/formulae.pdf

For the definitions, see pp. 359 ff.

One approach is the semantic approach (model theory), which is

appealing to many mathematicians, as the justification for the syntactic

inference is expressed with mathematical means.

But there is also another possibility, the syntactic approach.

In philosophy, a justification by a meta-theory (in which the

semantic evaluation takes place in model theory) is considered

problematic.

If a theory is justified by a meta-theory, than what justifies the meta-theory?

Such an approach would be considered as "outward" in philosophy.

The alternative is trying to express as much as possible within (!) the language,

this approach is called "immanent" (= within).

For this reason, the meta-perspective (bird's view from top) as used

with the turnstile symbol for provability should not be used for

expressing rules: "The turnstile (⊢) was eliminated and replaced by

the logical implication (⊃) [e.g., cf. pp. 303 ff. (K8025 = Deduction Theorem)

and Andrews, 2002, pp. 228 f. (5240 = Deduction Theorem)]."

http://www.owlofminerva.net/files/formulae.pdf (p. 12)

The turnstile may be used for metamathematics expressing properties

of a formal system after (!) setting up the language and logic, but should

not be used before, legitimizing or setting up the logic itself.

> Mario Carneiro

Kind regards,

Ken Kubota

Apr 16, 2017, 11:25:53 PM4/16/17

to Metamath

You have to be careful about what Metamath "is". Informally, people (including me) often associate it with the set.mm ZFC database implemented in the Metamath language. However, the Metamath language itself knows nothing about FOL/set theory and is not restricted to it. The simplicity I refer to is that of the Metamath computer language, which is specified in 4 pages starting at p. 92 of the Metamath book. Different systems of logic can be implemented in that computer language, for example Mario Carneiro's HOL database at http://us.metamath.org/holgif/mmhol.html . Any Metamath proof verifier will work without modification regardless of what logic is implemented in the Metamath language.

I think what you are really trying to compare is ZFC vs. R0, not Metamath vs. R0. I don't know of any reason that R0 could not be implemented in a Metamath database.

As for ZFC vs. type theory, that is a different issue that isn't really related to the Metamath language per se. I'm not familiar with Q0 that R0 is based on (I don't have access to Andrews' book right now). However, an implementation of R0 in the Metamath language would provide one kind of objective comparison of the complexity of say ZFC vs. R0.

The connection between HOL (and I would assume R0?) and "standard mathematics" (ZFC) is somewhat complex. The derivation of standard FOL and some ZFC axioms in Mario's HOL database has some 200 theorems. That isn't to say that HOL is not a beautiful thing, and very powerful for its theorem-proving purpose. However, HOL doesn't produce exactly the ZFC axioms. For example, as I understand it, cardinals beyond a certain size cannot be represented; whether that is an issue depends on the area of mathematics one is interested in studying.

Norm

Apr 16, 2017, 11:37:42 PM4/16/17

to Metamath

On Sunday, April 16, 2017 at 10:47:34 AM UTC-4, Ken Kubota wrote:

[...]

2.

I'm not familiar with Metamath in detail, and might be mistaken

and apologize for this.

Of course, ZFC is a very expressive, but for general reasons,

I consider type theory the better approach for expressing

mathematics than (axiomatic) set theory.

What is an example of mathematics you think it can express better?

Type theory prevents the paradoxes by means of the language,

as it makes the classification of mathematical objects explicit.

The concept of (axiomatic) set theory then appears as a rather

auxiliary solution, since with the distinction between classes and

sets first all inferences are forbidden, and with the axioms some

are allowed again. This renders the set of axioms as historically

arbitrary (the mathematics currently used), as shown with later

additions like axioms for large cardinals.

So (axiomatic) set theory does not provide a systematic solution

like type theory, which uses the means of the formal language

for preventing the paradoxes as intended by Russell.

If by paradox you mean inconsistency, then by Godel's incompleteness theorem any system powerful enough to express arithmetic cannot be proved to be consistent. That includes type theory as well as ZFC.

Norm

Apr 17, 2017, 9:27:47 AM4/17/17

to meta...@googlegroups.com, Ondřej Kunčar, Andrei Popescu, Prof. Peter B. Andrews

Hi Norman,

Let me copy to Ondřej Kunčar and Andrei Popescu, as in section 2

I refer to their paper.

> Am 17.04.2017 um 05:37 schrieb Norman Megill <n...@alum.mit.edu>:

>

>

>

> On Sunday, April 16, 2017 at 10:47:34 AM UTC-4, Ken Kubota wrote:

> [...]

>> 2.

>>

>> I'm not familiar with Metamath in detail, and might be mistaken

>> and apologize for this.

>>

>> Of course, ZFC is a very expressive, but for general reasons,

>> I consider type theory the better approach for expressing

>> mathematics than (axiomatic) set theory.

>

> What is an example of mathematics you think it can express better?

1.

Besides large cardinals, I do not have a concrete example,

as my argument is of general nature. But it should be possible

to construct mathematical objects, that, like large cardinals,

go beyond ZFC, by assuming additional axioms (as done for

large cardinals).

My criticism of ZFC (or axiomatic set theory in general) is,

that it positively introduces certain allowed mathematical objects

(always leaving other construable mathematical objects unregarded),

instead of systematically drawing the general line of distinction

between definitions that lead to inconsistency (paradoxes),

and those that do not.

>> Type theory prevents the paradoxes by means of the language,

>> as it makes the classification of mathematical objects explicit.

>

>> The concept of (axiomatic) set theory then appears as a rather

>> auxiliary solution, since with the distinction between classes and

>> sets first all inferences are forbidden, and with the axioms some

>> are allowed again. This renders the set of axioms as historically

>> arbitrary (the mathematics currently used), as shown with later

>> additions like axioms for large cardinals.

>>

>> So (axiomatic) set theory does not provide a systematic solution

>> like type theory, which uses the means of the formal language

>> for preventing the paradoxes as intended by Russell.

>

> If by paradox you mean inconsistency, then by Godel's incompleteness theorem any system powerful enough to express arithmetic cannot be proved to be consistent. That includes type theory as well as ZFC.

>

> Russell's paradox is not an issue in ZFC because its axioms are specifically designed to prevent it i.e. some classes are too large to qualify as sets.

2.

Both type theory and (axiomatic) set theory were introduced in 1908

in order to avoid Russell's paradox (or similar paradoxes).

But, as argued above, (axiomatic) set theory has a preliminary

character, as the set of axioms is rather arbitrary.

Type theory tries to prevent the paradoxes in a systematic way,

i.e., by means of the formal language, such that all mathematical objects,

which do not lead to paradoxes, can be expressed within the

formal language (without having to assume additional axioms).

By tracking the dependencies, the paradoxes (negative self-reference)

– and only these (!) – are prevented by the means of the formal language.

ZFC avoids the paradoxes simply by limiting the reasoning to

sets construable by the ZFC axioms, which represent more or less

the mathematics mostly used, but not all of mathematics which

is in principle possible.

For Isabelle/HOL, in order to avoid a (negative) self-reference

(Kunčar/Popescu: "circularity") as construed in example 2 of

http://andreipopescu.uk/pdf/ITP2015.pdf

http://doi.org/10.1007/978-3-319-22102-1_16

Ondřej Kunčar and Andrei Popescu introduced some kind of

bookkeeping mechanism to keep track of the dependencies.

However, as argued above, the natural approach of type theory

is to specify the formal language such that paradoxes (and only

these) cannot be expressed at all (as they violate type restrictions).

This also means that non-logical axioms (e.g., pairs, unions,

Axiom of Infinity, Axiom of Choice) should be avoided as part

of the logic, and introduced as part of a definition instead.

For example, the three group axioms are part of the

definition "Grp" in R0, see p. 362 of

http://www.owlofminerva.net/files/formulae.pdf

Moreover, this has the advantage that contradictory axioms do

not render the logic inconsistent as a whole, but only result

in an empty set (since no object can fulfill the definition).

R0 has four axioms, which are logical axioms only,

see pp. 353 ff. of

http://www.owlofminerva.net/files/formulae.pdf

The question is, how to define the notion of mathematics, and

to find an adequate formal representation. Andrews' Q0 has

substitution as the single rule of inference (Rule R), from which

he obtains lambda-conversion and reflexivity (A=A; for any A),

and most of standard mathematics. For a number of reasons,

I decided to make the latter independent, such that there

are basically three rules, substitution (§s), lambda-conversion (§\),

and reflexivity (§=), see p. 12 of

http://www.owlofminerva.net/files/formulae.pdf

I would basically argue, that mathematics is everything which

can be obtained by substitution and lambda-conversion, and

not just the limited area allowed by the (historically arbitrary)

ZFC axioms.

Let me copy to Ondřej Kunčar and Andrei Popescu, as in section 2

I refer to their paper.

> Am 17.04.2017 um 05:37 schrieb Norman Megill <n...@alum.mit.edu>:

>

>

>

> On Sunday, April 16, 2017 at 10:47:34 AM UTC-4, Ken Kubota wrote:

> [...]

>> 2.

>>

>> I'm not familiar with Metamath in detail, and might be mistaken

>> and apologize for this.

>>

>> Of course, ZFC is a very expressive, but for general reasons,

>> I consider type theory the better approach for expressing

>> mathematics than (axiomatic) set theory.

>

> What is an example of mathematics you think it can express better?

Besides large cardinals, I do not have a concrete example,

as my argument is of general nature. But it should be possible

to construct mathematical objects, that, like large cardinals,

go beyond ZFC, by assuming additional axioms (as done for

large cardinals).

My criticism of ZFC (or axiomatic set theory in general) is,

that it positively introduces certain allowed mathematical objects

(always leaving other construable mathematical objects unregarded),

instead of systematically drawing the general line of distinction

between definitions that lead to inconsistency (paradoxes),

and those that do not.

>> Type theory prevents the paradoxes by means of the language,

>> as it makes the classification of mathematical objects explicit.

>

>> The concept of (axiomatic) set theory then appears as a rather

>> auxiliary solution, since with the distinction between classes and

>> sets first all inferences are forbidden, and with the axioms some

>> are allowed again. This renders the set of axioms as historically

>> arbitrary (the mathematics currently used), as shown with later

>> additions like axioms for large cardinals.

>>

>> So (axiomatic) set theory does not provide a systematic solution

>> like type theory, which uses the means of the formal language

>> for preventing the paradoxes as intended by Russell.

>

> If by paradox you mean inconsistency, then by Godel's incompleteness theorem any system powerful enough to express arithmetic cannot be proved to be consistent. That includes type theory as well as ZFC.

>

> Russell's paradox is not an issue in ZFC because its axioms are specifically designed to prevent it i.e. some classes are too large to qualify as sets.

Both type theory and (axiomatic) set theory were introduced in 1908

in order to avoid Russell's paradox (or similar paradoxes).

But, as argued above, (axiomatic) set theory has a preliminary

character, as the set of axioms is rather arbitrary.

Type theory tries to prevent the paradoxes in a systematic way,

i.e., by means of the formal language, such that all mathematical objects,

which do not lead to paradoxes, can be expressed within the

formal language (without having to assume additional axioms).

By tracking the dependencies, the paradoxes (negative self-reference)

– and only these (!) – are prevented by the means of the formal language.

ZFC avoids the paradoxes simply by limiting the reasoning to

sets construable by the ZFC axioms, which represent more or less

the mathematics mostly used, but not all of mathematics which

is in principle possible.

For Isabelle/HOL, in order to avoid a (negative) self-reference

(Kunčar/Popescu: "circularity") as construed in example 2 of

http://andreipopescu.uk/pdf/ITP2015.pdf

http://doi.org/10.1007/978-3-319-22102-1_16

Ondřej Kunčar and Andrei Popescu introduced some kind of

bookkeeping mechanism to keep track of the dependencies.

However, as argued above, the natural approach of type theory

is to specify the formal language such that paradoxes (and only

these) cannot be expressed at all (as they violate type restrictions).

This also means that non-logical axioms (e.g., pairs, unions,

Axiom of Infinity, Axiom of Choice) should be avoided as part

of the logic, and introduced as part of a definition instead.

For example, the three group axioms are part of the

definition "Grp" in R0, see p. 362 of

http://www.owlofminerva.net/files/formulae.pdf

Moreover, this has the advantage that contradictory axioms do

not render the logic inconsistent as a whole, but only result

in an empty set (since no object can fulfill the definition).

R0 has four axioms, which are logical axioms only,

see pp. 353 ff. of

http://www.owlofminerva.net/files/formulae.pdf

The question is, how to define the notion of mathematics, and

to find an adequate formal representation. Andrews' Q0 has

substitution as the single rule of inference (Rule R), from which

he obtains lambda-conversion and reflexivity (A=A; for any A),

and most of standard mathematics. For a number of reasons,

I decided to make the latter independent, such that there

are basically three rules, substitution (§s), lambda-conversion (§\),

and reflexivity (§=), see p. 12 of

http://www.owlofminerva.net/files/formulae.pdf

I would basically argue, that mathematics is everything which

can be obtained by substitution and lambda-conversion, and

not just the limited area allowed by the (historically arbitrary)

ZFC axioms.

Apr 17, 2017, 9:30:58 AM4/17/17

to meta...@googlegroups.com, Prof. Peter B. Andrews

> Am 17.04.2017 um 05:25 schrieb Norman Megill <n...@alum.mit.edu>:

>

> You have to be careful about what Metamath "is". Informally, people (including me) often associate it with the set.mm ZFC database implemented in the Metamath language. However, the Metamath language itself knows nothing about FOL/set theory and is not restricted to it. The simplicity I refer to is that of the Metamath computer language, which is specified in 4 pages starting at p. 92 of the Metamath book. Different systems of logic can be implemented in that computer language, for example Mario Carneiro's HOL database at http://us.metamath.org/holgif/mmhol.html . Any Metamath proof verifier will work without modification regardless of what logic is implemented in the Metamath language.

>

> I think what you are really trying to compare is ZFC vs. R0, not Metamath vs. R0. I don't know of any reason that R0 could not be implemented in a Metamath database.

This corresponds to Freek Wiedijk's classification at

http://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf (p. 9)

> As for ZFC vs. type theory, that is a different issue that isn't really related to the Metamath language per se. I'm not familiar with Q0 that R0 is based on (I don't have access to Andrews' book right now). However, an implementation of R0 in the Metamath language would provide one kind of objective comparison of the complexity of say ZFC vs. R0.

https://plato.stanford.edu/entries/type-theory-church/#ForBasEqu

Also, the very first presentation [Andrews, 1963, pp. 345 f., 350] is available online:

http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52124.pdf

Q0 is, like Mike Gordon's HOL, a variant of Church's Simple Theory

of Types [Church, 1940], which can be obtained at

http://www.jstor.org/stable/2266170

This is the classical reference, as Church extensively uses

lambda notation for expressing mathematics.

However, in order to understand the expressiveness of Q0, one should have

a look at the syntactic part [Andrews, 2002, pp. 201–237] of chapter 5 of

Andrews' 2002 textbook (2nd edition, ISBN 1-4020-0763-9), or at least the

1st edition [Andrews, 1986, pp. 154–185] (ISBN 0-12-058535-9 / 0-12-058536-7).

For the references, please see:

http://doi.org/10.4444/100.111

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu