Comparison of Metamath and Q0 – Fwd: Publication of the Mathematical Logic R0: Mathematical Formulae

[Ken Kubota]

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

[vvs]

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?

[Ken Kubota]

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

Kind regards,

Ken Kubota

____________________

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

[vvs]

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.

[Ken Kubota]

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

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.

My work has been published and announced for only a few days,
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)

[Mario Carneiro]

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

[vvs]

воскресенье, 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?

[Ken Kubota]

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

[Norman Megill]

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

[Norman Megill]

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.
 

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.
 
Norm

[Ken Kubota]

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.

[Ken Kubota]

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

Thanks for pointing out that Metamath is, like Isabelle, a logical framework.

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.

A short online description of Q0 can be found at
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