The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

[Due to the Coq mailing list size restrictions, this email is split in two parts.]

Von: Ken Kubota <mail AT kenkubota.de>

Betreff: Metamath, Isabelle/HOL, Coq, Lean (General debate initiated by Kevin Buzzard on formalizing mathematics: Where is the fashionable mathematics?) – Re: [Metamath] Are we listening?

Datum: 23. Februar 2020 um 16:24:48 MEZ

An: metamath AT googlegroups.com

Kopie: cl-isabelle-users AT lists.cam.ac.uk, "hol-info AT lists.sourceforge.net" <hol-info AT lists.sourceforge.net>, coq-club AT inria.fr, "Prof. Kevin Buzzard" <k.buzzard AT imperial.ac.uk>, "Prof. Peter B. Andrews" <andrews AT cmu.edu>, "Prof. Lawrence C. Paulson" <lp15 AT cam.ac.uk>, "Prof. Jeremy Avigad" <avigad AT cmu.edu>, Leonardo de Moura <leonardo AT microsoft.com>, Daniel Selsam <daniel.selsam AT microsoft.com>

Let me comment on Kevin Buzzard's intervention (blog: xenaproject.wordpress.com, website: wwwf.imperial.ac.uk/~buzzard)

Where is the fashionable mathematics?

Posted on February 9, 2020
https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/

placed into the Metamath list by vvs <vvs009 AT gmail.com> at

https://groups.google.com/d/msgid/metamath/6478d27f-2d3b-4296-9f95-9236562bd7e8%40googlegroups.com

Notes on Lean are placed in section A.2.,

notes on HOL and Isabelle/HOL in section B.

For Coq, see Kevin Buzzard's comment at https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/,

Freek Wiedijk's criticism quoted at https://owlofminerva.net/files/fom_2018.pdf#page=10,

and my comment on the Curry-Howard isomorphism at the end of section A further below.

A. General debate

Quote:

Am 10.02.2020 um 13:52 schrieb vvs <vvs009 AT gmail.com>:

He is trying to deliver this message to all, so I think people here might be interested too:

Each formal proof verification system (Lean, Coq, Isabelle/HOL, UniMath, all of the others) has its own community, and it is surely in the interests of their members to see their communities grow. These systems are all claiming to do mathematics, as well as other things too (program verification, research into higher topos theory and higher type theory etc). But two things have become clear to me over the last two years or so:

1. There is a large community of mathematicians out there who simply cannot join these communities because the learning curve is too high and much of the documentation is written for computer scientists.
2. Even if a mathematician battles their way into one of these communities, there is a risk that they will not find the kind of mathematics which they are being taught, or teaching, in their own department, and there is a very big risk that they will not find much fashionable mathematics.

My explicit question to all the people in these formal proof verification communities is: what are you doing about this?

Full post is here: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/

The historical approach of formalizing all (or all important) mathematical knowledge is the QED Project: mizar.org/qed

My proposal for a solution consists of two steps:

1. Creating a formal language according to Andrews' notion of expressiveness, i.e., using the simplest, weakest means in order to express all of mathematics in a natural way.

This would result in a Hilbert-style system with lambda notation (and use of the description operator) such as Andrews' logic Q0:

"Q0 requires only two basic types [...] and only two basic constants [...], thus reducing the language of formal logic and mathematics to a minimal set of basic notions."

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html

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

• Peter B. Andrews on expressiveness as the main criterion for the design of Q0: “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.]

https://owlofminerva.net/files/fom_2018.pdf#page=5

"A bottom-up representation (which is better suited for foundational research) 

is clearly a Hilbert-style system: It has the elegance of having only a few 

rules of inference (in Q0 even only a single rule of inference - Andy Pitts: 

"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]). 

Metatheorems are not expressible within the formalism; the metatheorems are 

literally "meta" ("above" - i.e., outside of - the logic). In software 

implementations of Q0 or descendants (Prooftoys by Cris Perdue or my R0 

implementation), the metalogical turnstile (⊢) symbol is replaced by the 

logical implication, which shows the tendency to eliminate metalogical elements 

from the formal language."

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-May/msg00013.html

Adding dependent types (or at least type abstraction) results in R0, in which abstract algebra (here: group theory) can be expressed very naturally:

https://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/#type_abstraction

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00045.html

(Note that Metamath isn't really Hilbert-style, in my opinion, since it can express metatheorems. It seems to start directly at a higher level, like all logical frameworks.

A true Hilbert-style system consists only of the (mathematical) object language. So I disagree with Mario Carneiro at this point:

https://groups.google.com/d/msg/metamath/DRMh8ZPA6Mo/10_2n9pfDgAJ )

2. Implementing a natural deduction variant of the formal language created in step one (i.e., making metamathematical theorems symbolically expressible as required for automation):

https://sourceforge.net/p/hol/mailman/message/36654754/

Maybe one should go to the other extreme in this step and establish/use a logical framework (e.g., Twelf, Isabelle):

"A top-down representation (which is better suited for applied mathematics: 

interactive/automated theorem proving) is either a natural deduction system 

(like HOL) or a logical framework (like Isabelle): It has a proliferation of 

rules of inference (e.g., eight rules for HOL [cf. Gordon and Melham, 1993, pp. 

212 f.]). Metalogical properties (metatheorems) are expressible to a certain 

extent, e.g., using the turnstile (⊢) symbol (the conditionals / the parts 

before the turnstile may differ in the hypothesis and the conclusion), or the 

meta-implication (⇒) in Isabelle's metalogic M (not to be confused with the 

implication (⊃) of the object-logic), see

        http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf, p. 4

Unfortunately, the gain of expressiveness in terms of metalogical properties by 

making metatheorems symbolically representable is obtained at the price of 

philosophical rigor and elegance in expressing the underlying object logic 

(object language)."

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-May/msg00013.html

[Part 2 follows.]

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100