[FOM] Foundational Challenge

[Joe Shipman]

Although what Tim Chow says is right about metatheorems in general, I am talking here about a specific kind of metatheorem which is both a precisely stated and quotable theorem and easy to apply, namely “conservative extension results”.

“You’re allowed to assume Choice in proving arithmetical theorems because it’s been established that AC can be eliminated from any such proof” is eminently quotable and applicable. (I’m not sure how much proof-shortening is involved by adding the scheme “If AC implies Phi, then Phi” for arithmetical Phi to ZF, is anything known about this?)

Now that I think about it, the following caveat occurs to me.

In a relatively weak system, we can prove ZFC is a conservative extension of ZF for statements of low enough type. But are there weaker systems such that adding AC gives you new arithmetical theorems? Is ZC a conservative extension of Z For arithmetical statements? What about adding an appropriate form of Choice to second order arithmetic?

— JS

Sent from my iPhone

>> On Jan 25, 2020, at 12:55 AM, Timothy Y. Chow <tchow at math.princeton.edu> wrote:
>> 
>> 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