[FOM] Improving Set Theory

[Harvey Friedman]

So far, there seems to be general agreement that the classical set
theoretic foundation through ZFC and sugared ZFC is philosophically
coherent, whereas proposed alternatives are not philosophically
coherent. Undoubtedly there are attempts by some to make them
philosophically coherent, and it seems like a lot of good new ideas
are needed to accomplish this. I would think that the ideas needed
would be important and may be useful for other purposes, including
suggesting additional new powerful sugar for ZFC.

In order words, I envision progress along the lines of making
alternative foundations philosophically coherent probably would be
useful in Improving Set Theory as well. In this way, I could easily
imagine that classical set theoretic foundations still maintains its
decisive lead over the altheratnvies.

It is probably informative to look at the situation with regards to
proof assistant. No less than one of the leading figures, arguably
even the leading figure (I don't know enuf about all of the important
people in proof assistants to judge for myself) is advocating the use
of the classical set theoretic systems appropriately sugared for proof
assistants. This is John Harrison, and see

John Harrison. Let’s make set theory great again!
http://aitp-conference.org/2018/ slides/JH.pdf, 2018.

Steffen Frerix and Peter Koepke, Making Set Theory Great Again: The
Naproche-SAD Project,
http://aitp-conference.org/2019/abstract/paper%2026.pdf,

This second item above is rich in further references.

So I suspect that classical set theoretic foundations even dominates
certain central engineering projects as well as its primary
foundational purpose.

I have been thinking a bit about just where Proof Assistants is really
going. I gather from some comments I have seen that there is a bit of
a crisis, with regard to Proof Assistants aimed at creating formal
proofs.

The fact that it can be done with some practicality for big deep
theorems was an impressive achievement. There seems to be some
skepticism that one can get together the resources necessary to do it
for the biggest deepest theorems - being hard to argue on the basis of
need and major consequence. (I am distinguishing this from Proof
Assistance aimed at verifying the correctness of engineering systems).

So there is a particular line of research that seems probably
neglected and seems very interesting foundationally. Namely to develop
a robust notion or notions of SELF PROVING. More ambitiously,
measuring the LEVEL OF IDEAS needed to prove something. Level of ideas
zero would correspond to being Self Proving.

And what would we do after we get our hands on such robust definitions?

1. Prove that any proof of certain basic interesting propositions must
have a certain level of ideas.
2. Actually take some little areas of elementary mathematics and give
a treatment where the level of ideas used in this sense is
particularly low - in light of reworking of the material.

Harvey Friedman