First, I’m not (yet) an expert in formalized mathematics. I know Isabelle/ZF better, but have only overall view of Isabelle/HOL. Nevertheless I want to tell my opinion on typed (such as HOL) vs. untyped (such as Isabelle/ZF) systems.
Slawomir Kolodynski converted me into his religion of doing formalized math with Isabelle/ZF and answering “yes” to the question “Should the next generation of proof assistants be based on ZFC set theory?”, but now I resign.
The conclusion I drew recently: Doing math in untyped formalized systems such as ZFC is wrong. We need a typed system.
I drew this conclusion after my attempt to write a new version of “Funcoids and Reloids” (a draft article in the field of General Topology) presented on my site. I had the following trouble: Informal mathematics has no concept of types (not counting informal notion “dependent on the context” which is too raw to be used in complex enough cases like this my article). Without types it requires as I’ll show below to quality operations with a symbol denoting the context in which the operation is done. For an example, I need to write instead of just to denote the meet operation on the lattice . The very trouble is with overlapping lattices, where it’s impossible to deduce which lattice is meant in as and may belong do different lattices.
Thus I did it in a wrong way, knowing that it is a wrong way. The reason I indeed has done it wrong is that there are just no concept of types in informal mathematics as it is presented customary. There are no way to do it in a right way without first introducing a formal system with types, which I cannot do in this article, because it is not an article about logic.
In this regard formalized math has an advantage over informal math, as statements of theorems and definitions can be write more concise in formal math thanks to types.
[This version of my article deleted as it is useless because my idea expressed in this post is wrong, see a comment.]
An example notation from the above mentioned article:
(here is roughly saying the set of filters on a set ordered reverse to set theoretic inclusion and means the set of funcoids from a set to a set , for our consideration it does not matter what exactly are funcoids).
See long, dependent on arguments qualifiers on every operation? It is a thing we need to get rid of. See the above mentioned article for more examples with such long verbose formulas.
As I’ve said above Slawomir Kolodynski converted me into his religion of doing formalized math with Isabelle/ZF, but now I resign. My new ideology is that we should try to make formalized math in Isabelle/HOL (including HOLZF).
Speculating in an area I do not know as an expert, I think we should do sets (in the sense of ZF sets) in HOLZF, but wrap some of them into HOL types.
Before ZF was seeming feasible for me, because I introduced the concept of generalization in the framework of ZF. This my result was looking for me as a solution of all typing problems. Now I realize, it isn’t. The above mentioned General Topology article cannot be written concisely in ZF without types.
Indeed a problem which my theory of generalization solves well is whole numbers generalizing natural numbers, rational numbers generalizing whole numbers, real numbers generalizing rational numbers, complex numbers generalizing real numbers, etc.
I does not work well with the theory of lattices and filters (for the reason that for example as lattice meet operation may mean different for the same arguments of the operation, because its meaning is different for different (overlapping) lattices).
Maybe we need to invent some new system having advantage of both untyped and typed systems. As a temporary solution I suggest as I wrote above to wrap HOLZF set values inside strong types. Is this working well? I don’t know.
Finally, I call you to discuss this topic in blogs and mailing lists.