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

[Ken K. <ma...@ke...>]

Let me comment on Kevin Buzzard's intervention (blog: xenaproject.wordpress.com <http://xenaproject.wordpress.com/>, website: wwwf.imperial.ac.uk/~buzzard <http://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/ <https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/>
placed into the Metamath list by vvs <vv...@gm...> at
	https://groups.google.com/d/msgid/metamath/6478d27f-2d3b-4296-9f95-9236562bd7e8%40googlegroups.com <https://groups.google.com/d/msgid/metamath/647...@go...>

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/ <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 <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 <vv...@gm...>:
> 
> 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:
> 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.
> 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 <http://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://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html>
	https://plato.stanford.edu/archives/sum2018/entries/type-theory-church/#ForBasEqu <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 <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 <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://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 <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 <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/ <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 <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 <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-May/msg00013.html>

According to the concept of expressiveness, unnecessary types or constants should be avoided.

The list type as implemented in Lean
	https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#types-as-objects <https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#types-as-objects>
is unnecessary, as the definition of ordered pairs [Andrews 2002 (ISBN 1-4020-0763-9), p. 208] can be used to establish vectors, which may serve as lists:
	• Ordered Pairs With One Type Variable
	https://www.owlofminerva.net/files/formulae.pdf#page=376 <https://www.owlofminerva.net/files/formulae.pdf#page=376>
	• Vectors (Dependent Type Theory)
	https://www.owlofminerva.net/files/formulae.pdf#page=388 <https://www.owlofminerva.net/files/formulae.pdf#page=388>
See also: https://sourceforge.net/p/hol/mailman/message/35648326/ <https://sourceforge.net/p/hol/mailman/message/35648326/>

The Pi type, or dependent function type, as implemented in Lean
	https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#dependent-types <https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#dependent-types>
is unnecessary, as it simply can be expressed with type abstraction. The following statement is incorrect:
	"It is clear that cons α should have type α → list α → list α. But what type should cons have? A first guess might be Type → α → list α → list α, but, on reflection, this does not make sense: the α in this expression does not refer to anything, whereas it should refer to the argument of type Type. In other words, assuming α : Type is the first argument to the function, the type of the next two elements are α and list α. These types vary depending on the first argument, α."
	https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#dependent-types <https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#dependent-types> (emphasis as in the original)
It is overlooked that exactly this dependency ("does not refer to anything") can be expressed within the formal language by type abstraction (as suggested by Mike Gordon and as implemented in R0), which overcomes the strict separation of the term level from the type level:
	"In order to express this properly, type abstraction is required, which abstracts
from the concrete type ("their concrete presentations"). It creates a link between
the type and the term level, e.g.
	[\t.\*:ttt . a * id = a ]
or
	[\t.\x_{ttt} . a x id = a ]
for some identity element id.
Note that the variable t appears both at the term and at the type (subscript) level.

Standard HOL doesn't provide this feature, which was already suggested by
HOL founder Mike Gordon (he called it "'second order' λ-terms" [Gordon, 2001, p. 22]).
[...]
Group theory is best suited to demonstrate this, and I also chose group theory:
	http://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/#type_abstraction <http://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/#type_abstraction>
See the definitions "Grp" and "GrpIdy" there."
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00045.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00045.html>

A natural approach should avoid using the Curry-Howard isomorphism.
"All constructive foundations, including Coq, use the encoding of proofs based on 
the Curry-Howard isomorphism. But the concept of expressiveness yields the 
_natural_ expression of mathematics, hence the desire is not an _encoded_, but 
an _unencoded_ (direct) form of expression."
	https://sourceforge.net/p/hol/mailman/message/35648326/ <https://sourceforge.net/p/hol/mailman/message/35648326/>



B. Kevin Buzzard on Isabelle/HOL

"Where is the fashionable mathematics?
Posted on February 9, 2020

[...]

Isabelle/HOL users

Isabelle/HOL: Manuel Eberl is tirelessly generating 20th century analysis and analytic number theory. This is a highly respectable thing to do — he is planting the seeds. He is doing the basics. He cannot do it alone! Furthermore, HOL has no dependent types. Does this mean that there are entire areas of mathematics which are off limits to his system? I conjecture yes. Prove me wrong. Can you define the Picard group of a scheme in Isabelle/HOL? I am not sure that it is even possible to write this code in Isabelle/HOL in such a way that it will run in finite time, because you have to take a tensor product of sheaves of modules to define the multiplication, and a sheaf is a dependent type, and your clever HOL workarounds will not let you use typeclasses to define module structures on the modules which are values of the sheaves. So how will you do the tensor product? I don’t know. Does anyone know? Is this actually an interesting open research problem? Picard groups of schemes are used all over the place in the proof of Fermat’s Last Theorem. They are basic objects for a “proper mathematician”. What can Isabelle/HOL actually do before it breaks? Nobody knows. But what frustrates me is that nobody in the Isabelle/HOL community seems to care. Larry Paulson says that it’s easy to understand: different kinds of maths work best in different systems, and so you might want to choose the system depending on the maths you want to do. But do you people want to attract “working mathematicians”? Then where are the schemes? Can your system even do schemes? I don’t know. Does anyone know? If it cannot then this would be very valuable to know because it will help mathematician early adopters to make an informed decision about which system to use."
	https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ <https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/>

There is no question that Isabelle's theoretical foundation
	https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf <https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf>
is a scientific achievement and that Isabelle itself is an impressive piece of software.

But it is also clear that HOL's type system (and therefore Isabelle/HOL's type system) is poor.

Freek Wiedijk on the (current) HOL family: “There is one important reason why the HOLs are not yet attractive enough to be taken to be the QED system:
• The HOL type system is too poor. As we already argued in the previous section, it is too weak to properly do abstract algebra.
But it is worse than that. In the HOL type system there are no dependent types, nor is there any form of subtyping. (Mizar and Coq both have dependent types and some form of subtyping. In Mizar the subtyping is built into the type system. In Coq a similar effect is accomplished through the use of automatic coercions.)
For formal mathematics it is essential to both have dependent types and some form of subtyping.” [Wiedijk, 2007, p. 130, emphasis as in the original]
	https://owlofminerva.net/files/fom_2018.pdf#page=10 <https://owlofminerva.net/files/fom_2018.pdf#page=10>


Not even group theory (abstract algebra) can be expressed adequately – without circumlocations or workarounds –, since type abstraction is still missing, which HOL founder Mike Gordon suggested nearly 20 years ago for HOL:

14. Mike Gordon on explicit type variable quantification in HOL: “In future versions of HOL it is expected that there will be explicit type variable quantification [Melham, 1993b], i.e., terms of the form ∀α.t (where α is a type variable). The right hand side of definitions will be required to be closed with respect to both term and type variables. Melham has shown that this will make defining mechanisms much cleaner and also permit an elegant treatment of type specifications.” [Gordon, 2000, p. 175, fn. 7]
	https://www.owlofminerva.net/files/fom.pdf#page=6 <https://www.owlofminerva.net/files/fom.pdf#page=6>

17. Mike Gordon suggesting type abstraction for HOL: “The syntax and semantics of type variables are currently being studied by several logicians. A closely related area is the theory of ‘second order’ λ-terms like λα. λx:α. x, perhaps such terms should be included in the HOL logic.” [Gordon, 2001, p. 22]
	https://www.owlofminerva.net/files/fom.pdf#page=7 <https://www.owlofminerva.net/files/fom.pdf#page=7>


No visible attempts are made to implement type abstraction, neither in the current HOL4 nor in the Isabelle/HOL community, although this is the natural next step.

Andrei Popescu and Ondřej Kunčar have some philosophical intuition concerning (negative) self-reference.
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00074.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00074.html>


But I am not aware of any current attempts to overcome the obvious restrictions, which is not satisfying for a logician/mathematician.

Following Andrews' concept of expressiveness, i.e., naturally expressing all of formal logic and mathematics with a small set of symbols and rules (which includes what Kevin Buzzard calls "proper mathematics" or "fashionable mathematics"), it shouldn't be too difficult to implement type abstraction (and maybe full dependent types) in HOL4 and Isabelle/HOL.

Why doesn't this happen?



Kind regards,

Ken Kubota

____________________________________________________


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