[FOM] Foundational Challenge

[Timothy Y. Chow]

Joe Shipman wrote:

> b) it is an ARITHMETICAL result with a significantly shorter formal 
> derivation from first principles than is possible in ZFC 
> (?significantly? means ?more than the usual amount of work to translate 
> proofs formalized in Second Order Arithmetic into ZFC proofs?, which is 
> a well-understood quantity).

I don't have an example.  However, let me give a sketch of something that 
might lead to an answer. What follows may be somewhat wrong and is 
certainly not fully fleshed out, because I don't fully understand all the 
details.  But I think that one answer to Joe Shipman's question---if it 
exists---is likely to run approximately along the following lines, modulo 
garbles that I've introduced due to inadequate understanding.

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.

There is, of course, nothing mathematically interesting or difficult in 
principle about this "small step" from a specific construction to the 
isomorphism type.  Buzzard's concern can be thought of as an "engineering" 
concern.  As one builds up more and more mathematics, is the constant need 
to define isomorphism classes of mathematically interesting objects going 
to consume more and more effort?

Of the multiple answers to Buzzard's question, let me focus on Francois 
Dorais's.  He says that for any set A in the universe V of all sets, we 
can form a set-theoretic universe V(A) where we treat the elements of A as 
atoms.  As Dorais says:

    If A has additional structure, say it's a complete ordered field, then
    that structure will appear quickly in the hierarchy since we add all
    possible subsets at each step. Therefore A has all the same ordered
    field structure it originally had in V. Even completeness carries
    through since the subsets of A in V(A) come from subsets of the
    original A in V. The difference is that A has no internal structure in
    V(A) since we can't inspect the innards of atoms: all we can say about
    atoms is whether two atoms equal or not. The main kicker is that if A'
    is any isomorphic structure to A, then the isomorphism of A' and A
    lifts uniquely to an isomorphism of V(A') and V(A)!

In the comments, Andrej Bauer suggested that this kind of approach would 
not automatically scale up nicely, and upon further thought, Dorais seemed 
to agree:

    In my view, I prove a metatheorem: If phi(A) is a statement in the
    language of set theory meeting this and that syntactic requirement,
    then ZFC proves the universal closure of
    (∀A,A')(A≅A'->phi(A)->phi(A')). I'm being deliberately vague about the
    syntactic requirements and I originally thought that was the issue but
    I now think the issue is that I require phi(A) to be a formula in the
    language of set theory. I do not allow new symbols for then I would
    have to factor these into the (otherwise trivial) translation from V to
    V(A). This is important but it is not restrictive. It does, however,
    put additional burden on the "formalizer" who has to fully translate
    BSD (to keep the same example) in the language of set theory prior to
    applying the metatheorem. That is a massive task!

I don't fully grasp why this task is "massive," probably because I haven't 
gotten my hands dirty enough to understand intuitively how much 
engineering work is required.  Suppose, however, that Dorais (and Bauer) 
are correct that with a naive approach, a significant amount of 
engineering overhead is required, especially if we want to endow ZFC with 
abbreviation power.  What I have heard from UF proponents is that the 
univalence axiom precisely addresses this point, and greatly reduces the 
engineering overhead.

In terms of a concrete result where the univalence axiom is supposed to 
make a significant difference, I have heard cited the theorem that the 
homotopy group pi_n(S^n) = Z for all n.  This is the paper---

https://guillaumebrunerie.github.io/pdf/lb13cpp.pdf

---but unfortunately it's too technical for me to understand, so I'm not 
sure whether it's directly related to the alleged usefulness of the 
univalence axiom that I advertised above.  It's perhaps debatable whether 
pi_n(S^n) = Z is "arithmetical" but I kind of think it is.

Anyway, independently of the above claims about UF, I think it would be 
interesting if Harvey Friedman or someone else can confirm that a naive 
approach to encoding proofs in ZFC does run into engineering difficulties 
as outlined above, and if so, how they can be addressed with a cleverer 
approach.

Tim