[FOM] Maddy paper on what Foundations accomplish

[Timothy Y. Chow]

Thanks to Joe Shipman for drawing attention to Maddy's recent paper.  An 
alternative, and in my opinion better, link to the one that he provided is 
this one:

http://www.socsci.uci.edu/%7Epjmaddy/bio/What%20do%20we%20want%20-%20final

This is a well-written paper and Maddy's appealing terms for the various 
functions that a "foundation of mathematics" might perform are themselves 
an important contribution, in my opinion: Risk Assessment, Generous Arena, 
Shared Standard, Meta-mathematical Corral, Essential Guidance, and Proof 
Checking.  They provide a useful language for discussing the merits of 
various candidates for "foundations."  Some of the historical background 
was also new to me, and provided very useful perspective.

Having said that, I do have some criticisms of the paper.  The most 
serious one is that the claim towards the end of the paper that there is 
no computer-implemented proof assistant that is based on set theory is 
simply false.  Maddy is apparently unaware of Mizar.  This oversight might 
be easily repaired, except that Maddy seems to go further; she says, 
regarding Proof Checking,

   Set-theoretic foundations weren't designed for this purpose and
   aren't likely to help.

I'm sure that Harvey Friedman's reaction will be, "Them's fightin' words." 
It is true that Mizar has somewhat fallen by the wayside as type-theoretic 
proof assistants have surged in popularity, but it remains unclear (to me 
at least, and I'm sure many others) whether this is an "accident" in some 
sense, and whether set-theoretic proof assistants could be just as 
powerful and easy to use as type-theoretic proof assistants if people put 
enough effort into developing them.  There seems to be no reason in 
principle why they could not be, and I do not think that it is accurate to 
say that set-theoretic foundations were not designed with proof checking 
in mind.  Admittedly, they were not designed with *modern computers* in 
mind, but that does not mean that they were not designed with proof 
checking in mind.

This brings me to another (less serious) criticism of the paper, which is 
that Maddy seems to underplay the role of set-theoretic foundations as an 
adjudicator of correctness of proofs.  Maddy rightly rejects the notion 
that set theory acts as a "final court of appeal" in an *ontological* 
sense; nobody in their right mind would declare that concepts such as 
"string of symbols" or "natural number" are illegitimate mathematical 
concepts unless they can be ontologically grounded in set theory.  But 
implicit in the notions of "Risk Assessment" and "Shared Standard" is the 
idea that all mathematical proofs ought to be formalizable in one of the 
standard systems.  How else is one supposed to perform Risk Assessment, 
other than by some kind of reverse-mathematical analysis that determines 
where in the hierarchy of logical strength a particular proof falls?  How 
can something claim to be a Shared Standard, unless all proofs can be 
standardized?  Of course, nobody is *required* to perform a risk 
assessment or to explicitly formalize their mathematical proofs, but the 
point is that set theory is prepared to perform these functions if called 
upon to do so, and that means that it has to be designed to perform Proof 
Checking, at least in principle if not in practice.  People working in 
foundations have always had Proof Checking in the back of their mind; it 
is not something that sprang into being overnight when modern computers 
came into their own.

Another point I want to make is that Maddy does not seem to recognize that 
Generous Arena is somewhat in tension with Risk Assessment.  Generous 
Arena tends to tell us to maximize, while Risk Assessment tends to tell us 
to minimize.  Generous Arena tends to want to throw everything into to 
same kitchen sink so that we don't have to worry about what Maddy calls 
"import/export restrictions"; Risk Assessment wants us to cordon off 
consistent sandboxes with highly restricted capabilities.

My final point is not about Maddy's paper per se, but is rather a warning 
that when Voevodsky makes statements such as, "ZFC ... is not an adequate 
formalization of the set theory which is used in mathematics" or that 
homotopy type theory is "the first adequate formalization of the set 
theory that is used in pure mathematics," he is speaking as a partisan of 
homotopy theory.  That is, where he says or writes "mathematics," I would 
argue that we should mentally substitute "homotopy theory."  With this 
substitution, some of Voevodsky's claims that seem outrageously overstated 
become more defensible, and I think get closer to what he is really trying 
to say anyway.

Tim