[FOM] Foundational Challenge

[Harvey Friedman]

On Sat, Jan 11, 2020 at 12:57 AM Timothy Y. Chow
<tchow at math.princeton.edu> wrote:
>
> As a starting point, let me point to a MathOverflow question by Kevin
> Buzzard, a number theorist who has gotten interested in formalizing
> significant chunks of number theory in Lean.
>
>   https://mathoverflow.net/q/336191/
>
> Roughly speaking, Buzzard wants to know how to formalize proofs in an
> "efficient" manner, where the inefficiency that he's concerned about is
> the translation between specific constructions of mathematical objects,
> and their isomorphism types.  As an example, he gives the real numbers,
> which can be constructed in different ways---Dedekind cuts and Cauchy
> sequences being the most well known.  Now, "mathematically interesting"
> statements *about* the real numbers (say, the Birch--Swinnerton-Dyer
> conjecture, or BSD for short) never depend on whether you have constructed
> the reals one way or the other.  One constructs the reals, and from then
> on, by the term "the reals" one implicitly means the *isomorphism type* of
> the thing just constructed, rather than the thing that was actually
> constructed.
>
Let's make a distinction between three important features we would
like ZFC to have, or modify ZFC to attain them. This distinction is I
think rather important. These are of course not the only important
features.

1. If a normal mathematical statement without issues concerning its
formulation, is proved by mathematicians using commonly accepted
mathematical methods, then it has a formal proof in ZFC.

2. If a normal mathematical statement without issues concerning its
formulation, is proved by mathematicians using commonly accepted
mathematical methods, then it has a reasonably short formal proof in
ZFC.

3, If a normal mathematical statement without issues concerning its
formulation, is proved by mathematicians using commonly accepted
mathematical methods, then it has a reasonably short formal proof in
ZFC that can be read like very detailed normal mathematical
exposition.

I think it is now commonly accepted that 1) holds.It is 1) that is so
crucial for my Tangible Incompleteness project as I need to argue that
these New Tangible Incompleteness I am posting on momentarily, are not
provable by mathematicians using commonly accepted mathematical
methods. Note that to achieve this we really do need a decent
universal foundation for all of mathematics, rather than piecemeal
foundations for parts of mathematics.

So although 1 is most crucial for my 50+ year program, I am of course
quite interested in 2 and 3.

I'm not quite sure that 2 needs a modification of ZFC. Yes, ZFC itself
does not have any provisions for abbreviations. But the blowups this
causes might not be so bad in real world cases. I think this is sort
of an interesting question which may perhaps generate some interesting
technical work of independent interest.

Furthermore, 2 has historically been in doubt in the math community,
but less so now given all of the work done with provers.

With 3 it is obvious that serious sugar must be added to ZFC. I
believe that there is a huge difference between a major expert
sugaring ZFC than somebody sugaring ZFC who is not an expert, and
especially somebody sugaring ZFC who wants to believe that 3 is false.

So let's see if the relevant so called "obstacles" can be explained in
some familiar terms.

For 3, we definitely want to say pick a construction of the number
systems and then by some appropriate general purpose sugar, introduce
"the ordered ring of integers", for example, with a constant symbol,
C. We assert that C has the desired properties. We definitely want to
prove, even before introducing C, that any two things with the
required properties are isomorphic the sense of an appropriate
bijection. So later if we build a system and verify the critical
properties then we automatically know that that system is isomorphic
to C.

We go merrily along in this style. What is the simplest case where a
nasty time consuming situation arises? There may be some need to know
something about the isomorphisms themselves. Of course, here we might
as well prove that for two relevant gadgets, there is a unique
isomorphism.

Harvey Friedman