[FOM] New umbrella? (Freek Wiedijk)

[Freek Wiedijk]

Dear Paul,

>>On the other hand Coq is much more expressive for abstract
>>mathematics (abstract algebra, category theory, etc.) than
>>the HOLs
>
>Dear Freek, there's a considerable literature of papers that mix
>category theory and set theory quite seriously.  I recently
>coauthored some papers of this kind* so obviously I'm quite keen on
>the topic, and I'm slightly baffled by the perception of conflict
>between the two subjects.  Some of these papers (not mine) even use
>large cardinals.
>
>Are you saying there's no suitable proof assistant for formalizing
>results like this?

I was talking about the currently most popular systems:
Coq versus a couple of HOL-based systems.  The HOL-based
systems are certainly _less_ expressive.  For one thing
they lack dependent types.

So I was not doing Mizar justice in the post you quote.
Mizar has some serious defects: no good higher order abstract
syntax that you already want for basic calculus (just the
"Fraenkel-operator", which sucks), no empty types (that's
_stupid_ if you have dependent types), a _crazy_ system of
imports, a _crazy_ distinction between "Element of NAT" and
"natural number" that is hugely irritating, and finally it
provides no way to have users automate their proof while
good automation is not provided from Białystok either (no
linear arithmetic decision procedure, no easy inductive types
nor easy recursion over them, etc.), etc.  Still in Mizar
you certainly can do abstract mathematics very well, and
both set theory and category theory are seriously present.
And it has dependent types.  And in a way that's much more
pleasant than the way you get it in type theory.

I certainly can imagine an improved system, like Mizar but
with the most irritating flaws fixed and the more important
Coq/Isabelle goodies added on top, that would easily handle
abstract mathematics well, without needing to stomach the
ideosyncracies of type theory.

But such a system currently does not exist.  I think.

Freek