[FOM] Harrison Advocates ZFC

[Lawrence Paulson]

> On 1 Jun 2018, at 00:48, Jeremy Avigad <avigad at cmu.edu> wrote:
> 
> 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. 

Of course it is easy to underestimate the difficulties involved in building a system. Nevertheless, I would guess that the amount of effort and funding going into type theory exceeds the amount that went into set theory by an order of magnitude if not two. It's not unusual to encounter open hostility to set theory and classical logic combined with an air of moral superiority: “Oh, you aren’t constructive? And you don't store proof objects? Really?” And I have seen "proof assistant" actually DEFINED as "a software system for doing mathematics in a constructive type theory".

The academic interest simply isn't there. Consider the huge achievements of the Mizar group and the minimal attention they have received. Also, I think that my 2002 paper on proving the reflection theorem (and presented at CADE, a high-profile conference) was really interesting, but it had been cited only six times, and two of those are by myself.

I am certain that we would now have highly usable and flexible proof assistants based on some form of axiomatic set theory if this objective had enjoyed half the effort that has gone into type theory-based systems in the past 25 years.

Larry