[FOM] Maddy paper on what Foundations accomplish

Tue May 29 10:32:53 EDT 2018

I have quite a bit of experience with mechanising axiomatic set theory using automated proof methods. I have gone quite far, including recursive functions, ordinals, cardinals, many equivalents of the axiom of choice (done by an academic visitor), the reflection theorem and Gödel's constructible universe, including the absoluteness of L and the proof that V=L implies the axiom of choice. The main difficulty with respect to typed formalisms such as higher order logic is the absence of types, which makes it harder to simplify or decide arithmetic statements. All of this work was done using Isabelle/ZF. Isabelle's syntactic framework is higher order, so axiom schemes and proof schemes cause no difficulties. Both classes (syntactically, predicates) and class functions (syntactically, simply functions) are available.

Set theory for verification: I. From foundations to functions <http://www.cl.cam.ac.uk/~lp15/papers/Formath/set-I.pdf>
Set theory for verification: II. Induction and recursion <http://www.cl.cam.ac.uk/~lp15/papers/Formath/set-II.pdf>
Mechanizing set theory: cardinal arithmetic and the axiom of choice <http://www.cl.cam.ac.uk/~lp15/papers/Formath/AC.pdf>
The reflection theorem: a study in meta-theoretic reasoning <http://www.cl.cam.ac.uk/~lp15/papers/Formath/reflection.pdf>
The relative consistency of the axiom of choice — mechanized using Isabelle/ZF <http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=6560756&fulltextType=RA&fileId=S1461157000000449>

Very recently, Bohua Zhan in a remarkable project implemented axiomatic set theory afresh in a version of Isabelle extended with automation of his own design and developed a substantial chunk of mathematics in the system, culminating in the definition of the fundamental group for an arbitrary topological space.

https://arxiv.org/abs/1707.04757

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 has also been some work on implementing Bernays-Gödel set theory in pure first-order logic, first by Quaife and later by Belinfante. My impression is that the BG calculus is very inconvenient in practice.

https://pdfs.semanticscholar.org/e604/d23a1036ef18216a49024790a6a1131fd579.pdf <https://pdfs.semanticscholar.org/e604/d23a1036ef18216a49024790a6a1131fd579.pdf>
https://pdfs.semanticscholar.org/bb00/d08ed0adb2ed6ba6a42d3141f6295359803b.pdf
https://www.sciencedirect.com/science/article/pii/S0747717103000233

Larry Paulson

> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180529/4e8168cc/attachment-0001.html>