[FOM] 654: Theory Inspired by Automated Proving 1

[Lawrence Paulson]

> On 11 Feb 2016, at 07:55, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> However, many of you know that I am not shy of my deep skepticism
> about elaborate and over complicated foundational setups.
> 
> Recently, I had some extensive discussions with John Harrison  at a
> meeting, where I gave a talk:
> https://u.osu.edu/friedman.8/foundational-adventures/downloadable-lecture-notes-2/
> An Approach to the Formal Representation of Mathematical Propositions,
> February 3, 2016, Semantic Representation of mathematical Knowledge
> Workshop, Fields Institute, Toronto, Canada, 14 pages.
> DigialLibrary020716
> 
> John set up and extensively uses HOL Light with great success.
> http://www.cl.cam.ac.uk/~jrh13/papers/hollight.pdf
> 
> In HOL Light there is very light typing, although the types are hard,
> and not soft as in ZC. It is entirely clear that HOL Light can easily
> be replaced - and I say improved - by simply using ZC. You just don't
> gain much by using even the type structure in HOL Light. I will grant
> that a case can be made that you DO GAIN SOMETHING with these types in
> HOL Light if you are concerned with constructive mathematics issues.
> But even here, it seems that ZC can be ready adapted for this purpose
> as well, although there are some issues to be addressed.

Type systems are indeed fundamental in the world of interactive theorem proving. Some of the issues are purely philosophical, such as whether it is right to regard a line as a set of points, or to consider -1 to be a certain (infinite) set. But there are a great many practical reasons why practitioners have preferred typed formalisms. The obvious reason is that the type checker performs a strong and automatic confirmation that a given expression is well-formed. But probably a more significant reason is that, in combination with syntactic overloading, we can achieve a notation that is both expressive and tolerably readable. We can at least use the same symbol (+) for natural numbers, integers, complex numbers and even formal polynomials and matrices, and perhaps more impressively, we can set up the basics of limits and continuity in the abstract setting of topological spaces and successively refine them to metric spaces, Euclidean spaces, etc, etc while using the same symbols for them and without having to duplicate mathematical arguments in these different settings.

I’m only aware of two convincing implementations of set theory in proof assistants. One of them is Isabelle/ZF, which is my own work, and which provides a very nice environment for working in axiomatic set theory, but not for working in any other domain of mathematics. But notational issues cause problems very quickly. A textbook can use the same symbol (+) for both ordinal and cardinal addition, distinguishing the two by variable name conventions: this isn’t possible in a typeless framework. The system that gets it right is Mizar, which has an underlying set theory and a very elaborate and impressive soft type theory built above it. No one has managed to duplicate this, and Mizar itself, as far as I know, hasn’t been updated to be technologically competitive with modern systems.

If people want a set theory-based system, it would make sense to start with Mizar. There is no point confining oneself to ZC: the axiom of replacement does not cause any problems at all.

Larry Paulson