[FOM] Maddy paper on what Foundations accomplish

[Adam Naumowicz]

On Tue, 29 May 2018, Lawrence Paulson wrote:

> I'm not certain to what extent Mizar is an implementation of set theory. 
> I have heard it said that the de facto proof calculus of Mizar is typed 
> and that its relation to set theory is unclear. I can neither confirm 
> nor deny this claim.

There's a very recently published JAR paper on 'The Role of the Mizar 
Mathematical Library for Interactive Proof Development in Mizar' [1] which 
should definitely make the Mizar's relation to set theory clear enough.

Let me just quote two paragraphs from this paper:

"Owing to A. Trybulec's mathematical background deeply rooted in the 
Polish school of mathematics, the library was from the beginning based on 
set theory. However, in the first years of the MMLs existence, there were 
several experiments with the foundations of the library. Namely, there 
were attempts to build the library based on set theory with classes 
(MorseKelley) and without them (Zermelo-Fraenkel), as well as with the 
axiom of choice, or without it. Eventually, under the influence of 
formalizations in category theory, A. Trybulec decided on selecting the 
Tarski-Grothendieck set theory(...)"

and

"The idea was to keep the proof checking system independent from any 
particular set theory, and so the type Any was introduced to represent 
any arbitrary object, not necessarily being a proper set. This, in 
principle, enabled developing other libraries with different 
axiomatizations. However, the library developed in terms of TG contained 
an additional axiom that the type Any is also of type set. Since the 
interest in developing alternative libraries was rather small, later the 
type Any was completely removed from the axiomatic files in favor of 
using the type set alone."

So the key point here is to distinguish the Mizar proof checking system 
(with its proof language featuring e.g. the notion of soft types which 
allows to conveniently treat, say, a natural number as an integer, a real 
or complex number without any artificial 'gymnastics' in the 
formalization) and the library (MML) based on set-theoretic axioms, which 
has proved to be successful in setting ground to a number of quite 
advanced theories.

Adam Naumowicz

[1] https://link.springer.com/content/pdf/10.1007%2Fs10817-017-9440-6.pdf

===========================================================================
Dept. of Programming and Formal Methods      Fax: +48(85)738-83-33
Institute of Informatics                     Tel: +48(85)738-83-06 (office)
University of Bialystok                      E-mail: adamn at mizar.org
Ciolkowskiego 1M, 15-245 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
===========================================================================



>> On 27 May 2018, at 07:01, Joe Shipman <joeshipman at aol.com> wrote:
>>
>> In my opinion, there are three features which make “pure ZFC” unnecessarily difficult for computer proofs:
>> 1) the Kuratowski ordered pair (rather than having ordered pair as a primitive operation),
>>
>> 2) the construction of the integers with the X+1=U(X,{X}) operation rather than starting with them as atoms and providing arithmetic operations, and
>>
>> 3) the absence of class variables (or, equivalently, a sethood predicate), which rules out finite axiomatizations.
>>
>> The amount of work needed to write a compiler which translates proofs in such an expanded language into “pure ZFC” seems manageable and can be done once and for all, after which the issue of formalizing in Set Theory vs formalizing in a Type Theory mostly goes away.
>>
>> So perhaps “Proof Checking” isn’t such a big deal when comparing ZFC with Univalent Foundations. But maybe it is, I’ll wait and see what the experts on Univalent Foundations have to say.
>>
>> — JS
>>
>> Sent from my iPhone
>>
>>> On May 26, 2018, at 6:15 PM, 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
>>
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> https://cs.nyu.edu/mailman/listinfo/fom
>
>