[FOM] Improving Set Theory

[Lawrence Paulson]

I'm not aware of any crisis. People are plunging ahead and formalising great bodies of material in various systems. From time to time they run into obstacles, which generally they manage to get round through ingenuity. Sometimes the obstacle takes the form of a certain valuable feature not always doing what you want it to.

For example, Isabelle/HOL type classes are a convenient way to bundle up axiomatic properties that are shared by various mathematical entities. A while back, I ported the HOL Light library of quaternions. Little work was needed other than the quaternion construction itself: by proving a few statements, I was able to instantiate several type classes for its algebraic and topological properties, replacing several HOL Light files that were basically clones of proofs for other types. But you can't do that for constructions that don't yield types. I see people claiming that you can't do metric spaces (among many other things) in simple type theory because they often need to take parameters, but not everything has to be a type. It's just that the existence of type classes and type checking makes people want everything to be a type. But there are other ways of organising abstractions in Isabelle, locales in particular.

I don’t have a pithy summary of the mathematics available in Isabelle/HOL, but there is a comprehensive library online: https://www.isa-afp.org (Not all of this is mathematics however.)

Larry Paulson
On 14 Jan 2020, 01:23 +0000, tchow at alum.mit.edu, wrote:
>
>
> Another possible obstacle, which sounds like what Harvey is talking about,
> is the existence of specific theorems or bodies of knowledge that present
> technical obstacles for existing proof assistants. I've heard a little
> bit about such things, but not too much, and what I've heard does not
> suggest that types are the problem and we should switch to sets. If some
> people are saying that, I'd like to hear more details.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200114/c2d7d615/attachment-0001.html>