[FOM] Foundational Challenge

[Timothy Y. Chow]

Jamie Gabbay wrote:
>  *   Readers, even experienced ones, tend to treat meta-theorems of
>    fields that they are unfamiliar with, with suspicion.  So
>    specifically, even if a meta-theorem is true of ZF(A), the burden of
>    explaining to a randomly-chosen reader/referee what a FOM
>    meta-theorem even is (if required), and then convincing them that
>    this particular meta-theorem should be believed, sucks air away from
>    the interesting maths.  I've spent too much of my career trying to
>    make meta-theorems look easy, and they're just not: a good
>    meta-theorem tends to express a deep understanding of the global
>    structure of a theory, and this is not necessarily something a reader
>    can pick up in a hurry, unless they are very practised.

I have not taken the time to understand Gabbay's paper in detail, but I 
want to say that the above observations about metatheorems is a very 
important one that is often under-appreciated by those who have not 
"gotten their hands dirty" with actually proving metatheorems in gory 
detail.

Joe Shipman himself has made this point in other contexts on FOM before, 
when he objects to certain overly breezy statements by some mathematicians 
that something is "easy for experts to see," and when he pointedly asks 
for a precise metatheorem.  It is true that if we want to be rigorous then 
we need the metatheorem.  On the other hand, in defense of the breezy 
mathematicians, often there isn't a single metatheorem that one can prove 
once and for all that will cover every future contingency.  It often takes 
a non-trivial amount of work, and it's almost entirely uninteresting work 
from a mathematical point of view.

Similarly, there's a certain danger of being too breezy when asserting 
that certain things are "easy to do" in ZF, if we're claiming that it is 
not only easy in principle but easy in practice for the person who is 
tasked with getting the computer to agree.

A mathematician without any programming experience might be baffled why 
there are so many programming languages out there.  They're all equivalent 
(Turing-complete), so why can't we just sit down and solve the programming 
language design task once and for all and be done with it?  Do it right 
the first time, and we won't ever have to deal with new programming 
languages again.

In short, if our goal is Proof Checking (as opposed to other desiderata 
for a foundation for mathematics), then we have to be careful not to 
underestimate the work needed in practice to implement "mathematically 
uninteresting" metatheorems on a computer, and by the same token, we 
should not underestimate the value of technical tricks that substantially 
reduce the amount of work needed in practice.

In particular, I speculate, based on my limited understanding of the 
Univalence Axiom, that one of its main benefits is to reduce the 
"engineering burden" involved in fully formalizing certain kinds of 
theorems.

Tim