[FOM] Harrison Advocates ZFC

[Jeremy Avigad]

Friends,

I agree with John and Larry that the ideal proof assistant would be based
on ZFC, with enough practical infrastructure to support all the things we
need to do mathematics. The latter constraint is nontrivial, and satisfying
it amounts to designing flexible type-theory-like mechanisms to sit on top
of the type-free foundation. It is easy to underestimate the difficulties
involved in designing a useful and workable system, though. Lots of smart
people have worked on systems based on set theory, and I don't think we are
anywhere near having one that will satisfy the needs of ordinary
mathematicians. At present, systems based on type theory are closer to
being practically usable, at the expense of giving up the simplicity and
flexibility of set theory. That's a sacrifice I am willing to make in order
to see the interactive theorem proving make progress. But I am not dogmatic
about it: it is just an engineering tradeoff. I'd love to see progress made
on the set theory front.

Norm Megill's Metamath is a really interesting system, with a remarkably
small kernel and an amazing library.

  http://us.metamath.org/

The proof format is explicit and easy to check. There are lots of
independent checkers, and they check the library -- thousands of theorems
-- in seconds. Mario Carneiro has been a huge contributor; he has
formalized, among other things, the prime number theorem and Dirichlet's
theorem on primes in an arithmetic progression.

  https://arxiv.org/pdf/1608.02029.pdf

But using the system is like writing assembly code, and really only for
power users. It has a small and select user base, I don't think it will
reach a mainstream audience.

Cezary Kaliszyk's re-implementation of Mizar in the Isabelle framework
tries to address the shortcomings that Larry mentioned:

  https://dl.acm.org/citation.cfm?doid=2854065.2854070

Rather than trusting Mizar's opaque "by" command, all the (soft) typing
rules and inferences are made explicit.

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.

In my view, the best hope for a prover based on set theory comes from Bohua
Zhan:

  https://arxiv.org/abs/1707.04757
  https://www21.in.tum.de/~zhan/

Bohua is extremely smart and capable, and I have tremendous admiration for
him. The paper above is an impressive achievement, and does all the right
things: it offers new ideas and a prototype implementation. I hope he will
be continue that work.

Best wishes,

Jeremy
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180531/f7d05f68/attachment-0001.html>