[FOM] Harrison Advocates ZFC (tweaked)

[Harvey Friedman]

>From all accounts, John Harrison is viewed as one of the world's
leading producers of formally verified proofs. I have often heard the
opinion that he is the world's leading producer.

I found the pdf slides of his recent talk:

 http://aitp-conference.org/2018/slides/JH.pdf

This advocates in clear careful terms for the use of set theory as the
basis for proof assistants. In particular, for essentially

ZFC with free logic; or maybe
ZFC with urelements and free logic

where free logic allows undefined terms, with the usual smooth
convention that a compound term is defined if and only if all sub
terms are defined.

Harrison makes exactly the same case that I have consistently made and
continue to make - except with his vast knowledge and experience, and
my ignorance and inexperience.

Chow writes https://cs.nyu.edu/pipermail/fom/2018-May/021011.html

"  I'm sure that Harvey Friedman's reaction will be, "Them's fightin' words." "

So I am hijacking this very recent Harrison pdf for my "fighting words".

Also see recent FOM postings in the Archives from Shipman, Urban,
Paulson, Naumowicz.

************************

If you want an opinion from somebody who never never never ever ever
ever played in light mud, here it is.

1. I said in my own clumsy abbreviated way, in public, at a meeting in
Toronto on formalization of mathematics, exactly an abbreviated form
of this pdf by Harrison, to the giggles in the audience. Harrison
supported what I said, briefly, at the same public setting. Of course,
people tended to dismiss me with giggles - and justifiably so -
because they knew or at least suspected that I never played in mud.

2. File 1 under "all great minds think alike" (smile).

3. Any attempt to veer beyond tweaked ZFC (e.g., class theory)

CREATES MORE TROUBLE THAN IT IS WORTH

3. Having said this, I vote for

ZFC WITH URELEMENTS AND FREE LOGIC

4. ZFC is so formulated with schemes (separation, replacement, maybe
foundation, maybe some others), which use schematic relations or maybe
schematic relations and schematic functions. There is the logic rule
of FORMULA INSTANTIATION. No CLASS THEORY allowed.

5. This allows people to, e.g., develop the natural numbers with an
enormous range of possibilities. Even simultaneous, by defining
"natural numbers version 1, "natural numbers version 2", etcetera.
E.g.,

a. Von Neumann ordinals.
b. Primitive set NAT of urelements, maybe with primitive successor
function (either symbol or constant set for the function).
c. First proving that there exists a system with certain great
properties (Dedekind), and then instantiating it.
d. etcetera

One has to work out some allied issues - e.g., existential
instantiation as part of the logic - which is the appropriate kind of
free logic I always use.

6. But then ZFC with urelements and free logic becomes an umbrella,
supporting some closely related styles.

7. There emerges supporting software allowing automated translation
between different choices like a-d under this one Umbrella.

8. ALTERNATIVELY, in order to simplify our lives for now, we let
HARRISON appoint the blue ribbon very public HARRISON COMMITTEE of mud
slinging experts, decide with knowledge, experience, and oceans of
mud, what is the best way to proceed under this Umbrella in full
detail - with real time publicly available interactions, comments
allowed from others.

Harvey Friedman