[FOM] Maddy paper on what Foundations accomplish

[Josef Urban]

I think the reasons for Mizar being outnumbered and not much developed in
the past years are mostly social. If the paper was written in 2000, the
evidence in terms of large math formalizations done in various proof
assistants would look quite different. Also, many people today would like
to use a proof assistant based on set theory and the proof assistant
community is quite open to such ideas.

For example Bohua Zhan's auto2 project has been received well by the
Isabelle community and his set-theory formalizations are quite impressive.
Cezary Kaliszyk and Karol Pak are porting a lot of Mizar to a new Isabelle
Mizar-like object logic. John Harrison had a nice talk "Let's Make Set
Theory Great Again!" this year at AITP (the slides and video are linked
from the AITP web). Etc.

Josef

On Sun, May 27, 2018, 04:45 Timothy Y. Chow <tchow at alum.mit.edu> wrote:

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180529/92b0e857/attachment-0001.html>