[FOM] Harrison Advocates ZFC (tweaked)

[Lawrence Paulson]

I've looked at the slides and it is clear to me that John is (as always) firmly opposed to free logic, or what he calls "partial terms". He proposes a workaround to represent partial functions in set theory. This makes no sense to me: in set theory we don't need partial functions, as a function's domain can be an arbitrary set.

Various people's comments suggest a need for urelements or other syntactic extensions. These aren't necessary, and remember, even if you do achieve a slightly simpler encoding of the ordered pair (3,-1), you will never find a simple encoding of pi. All one needs is a sensible attitude to definitions, treating defined constants as atomic by default.

What we really need (and I can claim lots of experience here) is support in the prover for contextual information so that when we write say n*x, provided we have somehow declared n to be an integer and x to be a real, the correct adjustments will be made so that we get the right sort of multiplication. The proof assistant's automation also needs to take note of this contextual information. It's clear that Mizar has solved many of these problems already, but it's not clear how they were solved, so we may have to reinvent the wheel.

The other problem is funding. Sponsored research into dependent type theories has gone on in many countries for the past 35 years. Set theory is not in vogue and I would not be optimistic for anybody's chances with funding bodies. This will have to be a spare time exercise.

Larry

> On 30 May 2018, at 08:43, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> 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