[FOM] Harrison Advocates ZFC

[Lawrence Paulson]

> On 1 Jun 2018, at 00:48, Jeremy Avigad <avigad at cmu.edu> wrote:

> Larry himself has done a lot of good work on Isabelle/ZF, but when it came to porting John Harrison's complex analysis library, he chose to port it to Isabelle/HOL, even though porting it to Isabelle/ZF would have been a big inducement for people to work there. Maybe Larry can say something about that choice, and whether  he thinks developing complex analysis in Isabelle/ZF would have been feasible.

Isabelle/ZF is untyped, which unfortunately means it can't use Isabelle's linear arithmetic decision procedures, so arithmetic reasoning is difficult. We don't have a construction of the rational numbers, let alone the complex numbers. Overloading isn’t available, so we’d need different symbols for +, -, *, even 0 and 1, for each type of number. Sledgehammer is also not available. It's a chicken and egg problem: no users means no development means no users. When I feel an inclination to use Isabelle/ZF, it is invariably to investigate something in pure set theory.

> In my view, the best hope for a set-theory based prover comes from Bohua Zhan:
> 
>  https://arxiv.org/abs/1707.04757
>  https://www21.in.tum.de/~zhan/

This is an astonishing piece of work. He developed a new proof environment for ZF set theory from the axioms and constructed the reals (and much else) using nothing but automation of his own design. His setup is based around mathematical structures, so it has a lot of potential to support ordinary mathematics.

Larry