Best to equivocate on disciplinary norms
A close-ish reading of texts by Jody Azzouni and Jeremy Avigad
Pour la topologie étale, si proche de l’intuition classique, un garde-fou si imposant n’est pas nécessaire : il suffit de connaître (par exemple) le livre de Godement, et d’avoir un peu de foi. (Pierre Deligne, SGA 4 1/2, p. 1)
Although philosophy and mathematics have traditionally shared an extensive common vocabulary and enjoy many superficial similarities, the norms of their professional practice could not be more different. My first experience of a philosophy seminar, at the tender age of 17 or 18, left an indelible impression that has shaped my understanding of the aims of philosophy ever since, for better or worse; you might even call it a scar. The Oxford philosopher P. F. Strawson, the picture of an English gentleman, was trying to present the first lecture in his seminar course as visiting professor at Princeton, where I was an undergraduate. For reasons I have long forgotten I thought I should attend, and I took my place in the remotest of corners in a large room in a library. What I remember is that a tall, portly, and elegantly dressed graduate student interrupted Strawson repeatedly, challenging him after every sentence, while Strawson looked on imperturbably, with an amused curiosity that I have since understood to be the philosophical attitude, before responding in the same placid tone with which he had begun his lecture.
It will be important for the sequel to understand that this is a rational reconstruction of an event of which I understood nothing. It certainly could not have happened as I just described it, with an interruption after every single sentence. The word “portly” looks particularly dubious. My report is empirically false. But as an account of the primal scene it is certainly valid. What I understood at the time, and what subsequent experience has confirmed, is that the primary professional activity of philosophers is to explain why other philosophers are wrong. Indeed, my experience has convinced me that
(N) “the norm [of philosophical practice] is this”: All philosophers are wrong.1
Admitting this norm as a major premise we can then construct as many syllogisms as we like, e.g.
All philosophers are wrong.2
Frege was a philosopher.
Therefore, Frege was wrong.
Please understand that from my perspective there’s no shame in being wrong, when you’re a philosopher. On the contrary, it’s just that the standards of philosophy are so stringent as to make it impossible not to be wrong.3 Nevertheless, philosophy is indispensable in teaching us to think about how we think. As Jeremy Avigad wrote in 2011, arguing for more dialogue between philosophers and mathematicians,
If there is one thing that philosophers are traditionally good at, it is working with vague ideas and introducing the kind of conceptual clarity that can lead to philosophical and scientific progress.4
But there’s no right way of doing that, and professional philosophers know, or should know, that some other philosopher will come along sooner or later — maybe in the next 10 minutes — to explain where they went wrong.
It’s all in the game, as Omar Little would say. But the game of mathematics isn’t like that at all! It’s a rare event indeed when a lecture devotes even a few minutes to the mistakes of a previous author, and such an event can be devastating for the career of the author found to be in error. Moreover, even though it’s common enough for members of the audience to challenge the speaker’s claims, or to ask for clarification, this is (nearly) always with the aim of strengthening rather than rebutting the speaker’s work; the challenger does not expect to be included as a coauthor, much less to publish the questions in the form of a rebuttal.
The quote in the sentence in boldface above is modeled on a similar sentence found in a 2009 article5 by Jody Azzouni. Jeremy Avigad quoted this article (though not the sentence) in support of his claim that what I called the Central Dogma of Mathematical Formalism is the “standard view”; I critiqued this claim, and the Central Dogma itself, a few weeks ago. Here is Azzouni’s sentence that served as the model for mine:
The norm is this: There is a formal analogue of a purported informal mathematical proof or else the latter fails to be a proof.
and here is the one Avigad quoted:
…formalized proofs have become the norms of mathematical practice. …should it become clear that the implications (of assumptions to conclusion) of an informal proof cannot be replicated by a formal analogue, the status of that informal proof as a successful proof will be rejected.
Azzouni follows this a few lines later with a peremptory allusion to
the evident fact of the presence of the norm of formalized proof with respect to ordinary mathematical practice.
This fact is so evident for Azzouni, and by ricochet for Avigad, that no evidence is presented. I suspect strongly that’s simply because there is no evidence, since Azzouni’s supposed “norm” is as absent from my experience of “ordinary mathematical practice” as I suspect my norm (N) above is from Azzouni’s experience of philosophical practice. This is all I meant when I wrote, a few weeks ago, that a similar claim in Avigad’s article, regarding the relation between informal and formal proof, is “unsubstantiated”: that it is presented without evidence.
It’s possible that some 18th century philosophes proclaimed that to be a duck it no longer suffices to quack like a duck and to walk like a duck. Henceforward, they would have written, the norm is this: if the actions of the purported duck cannot be replicated by an analogue in Jacques de Vaucanson’s workshop, it will be rejected by the duck test. You may object to the analogy by noting that the organic duck is constrained by its DNA or some such thing, while mathematicians are free to change their disciplinary norms. Indeed we do, and more frequently than is dreamt of by philosophers (apart from those active on this site) — but we don’t do it at their behest!
Actually, I think my norm for philosophers has considerably more empirical support than Azzouni’s supposedly “evident” norm for mathematicians. Many philosophers, like the young upstart in Strawson’s seminar, certainly behave as if “all philosophers are wrong” is their disciplinary norm, whereas until about 15 years ago I’d never seen any behavior among mathematicians that would lend the least credence to Azzouni’s “evident fact.” Moreover, formalization as an explicit norm is still marginal among mathematicians, and I contend (but that is not today’s topic) that it will remain marginal as a component of mathematical practice, even if it becomes as user-friendly as the promoters of Lean and similar apparatus promise.
Since no centralized authority is empowered to enforce the disciplinary norms of mathematics,6 it’s really up to historians, and especially sociologists, to determine what our norms may be or may have been at any given time. However, neither philosophers nor mathematicians seem interested in consulting specialists in either discipline. It’s natural enough for a mathematical subculture with internally consistent norms — like the Bourbaki group, for example — to want them to be adopted more widely. But you may find it bizarre for philosophers to make claims, descriptive or prescriptive, about the norms of a group that has no reason to pay attention to them — unless you agree with my norm (N)!
Jeremy Avigad, now, in the ticklish position of being both philosopher and mathematician, might be expected to get in trouble conforming to two radically incompatible norms. His article “Reliability of mathematical inference” is in fact an attempt to reconcile the narratives around the relation of the “norm of formalized proof” for mathematics — the philosophers’ norm, which, as we’ve seen, is empirically as well as necessarily wrong — to the norm of “ordinary mathematical practice”7 in which the possibility of formalization plays no role.
Azzouni’s article was also an attempt to reconcile these narratives. The issue is well known, and it goes like this: if the “presence of the norm of formalized proof” is supposed to guarantee the correctness of an informal proof, how do we explain that this is never the “operant standard,” in Avigad’s language, especially when “most mathematicians cannot even state the axioms of a particular formal system”? I will not try to unpackage Azzouni’s complicated and thought-provoking answer to this question, which involves something called “inference packages,” but I would like to pause to take note of a very interesting point Azzouni makes in passing:
What needs to be explained … is how the mathematician’s apparent attention and focus on the surface features of ordinary mathematical proof enables such widespread and nearly universal compliance with the formalization norm.
Here, significantly, Azzouni does cite Donald MacKenzie, one of the most insightful of sociologists, who points out that the research for his book Mechanizing Proof “has been unable to find a case in which the application of mechanized proof threw doubt upon an established mathematical theorem.” A philosopher is recognized as successful not for finding correct answers — ruled out by norm (N) — but rather for finding and analyzing interesting questions. For Azzouni, explaining the phenomenon MacKenzie identified empirically is “the successor problem to Kant’s problem” (more or less the problem of how synthetic a priori mathematical proofs are possible). Focusing attention on this question, which the mathematical formalizers seem to have missed, proves that Azzouni is a successful philosopher.
Avigad’s article, published in the journal Synthèse — one of the leading international journals specialized in philosophy of science — takes the narrative along more familiar lines:
at least relative to a choice of axiomatic foundation, the view I am expounding here amounts to this. When someone in the mathematical community makes a mathematical claim, it is generally possible to express that claim formally, in the sense that logically adept and sufficiently motivated mathematicians can come to agreement that the formal claim expresses the relevant theorem. One justifies an informal claim by proving it, and if the proof is correct, with enough work it can be turned into a formal derivation.
I have added the emphasis. It suggests that Avigad is claiming — “expounding” — that the Central Dogma is “generally” valid but is not reflected in “ordinary mathematical practice,” mainly because it’s impractical (too much work). The citation from Avigad’s article that I characterized here as “militant,” as well as unsubstantiated, is contained in the same paragraph as the last quotation:
…an informal mathematical statement is a theorem if and only if its formal counterpart has a formal derivation. Whether or not a mathematician reading a proof would characterize the state of affairs in these terms, a judgement as to correctness is tantamount to a judgment as to the existence of a formal derivation, and whatever psychological processes the mathematician brings to bear, they are reliable insofar as they track the correspondence.
I have explained above why this account of the relation between formal and informal proofs is unsubstantiated. Here I will add that the obsession of some (or most?) philosophers of mathematics with formal proof is misguided,8 unless the purpose is to illustrate norm (N).
On the other hand, whether or not the characterization of the quotation as “militant” is also justified largely hinges on whether
he believes the claim he is “expounding” or is just presenting it as the “standard view” among philosophers of mathematics;
if the former is true, whether he believes that formalization should be the disciplinary norm for mathematics; and
assuming he does, whether he plans to do something about it.
The actual expounding in the Synthèse article is hedged with expressions like “on the logical story” and “the thought goes” that suggest that Avigad is just giving an impartial account of the “standard view.” Avigad seems to contradict this interpretation, however, when he comes out and says that “I believe the standard view is essentially correct,” and amplifies his belief9 with sentences like
We are looking for a clarification of mathematical standards of correctness and insight as to how these standards are met, and vague appeals to meaning and understanding are at best optimistic gestures towards a more satisfying account.… If the inquiry stops there, we have clearly failed.10
which rejects one alternative; and that viewing informal rigor and formalizability as completely independent
requires us to provide an independent characterization of rigor and provide some other explanation of what it means for an informal proof to be correct.
Later he writes that
…we need to understand how our mathematical practices can manage to reliably (though imperfectly) warrant the existence of formal derivations…
Although this talk of “failing” and “requiring” and “needing” strikes me as militant, and by the last sentence Avigad has followed Azzouni in taking as “evident” that the Central Dogma is the disciplinary norm of mathematicians, the “we” in the above sentences must refer to philosophers11 and is not an injunction directed at, nor an attempt to ventriloquize, mathematicians.
On the other hand, taking charge of a $20,000,000 Center for Formal Mathematics, funded by a billionaire whose stated aim is to train a “very large distributed community” to “transform all kinds of things” in the service of a “paradigm” based on formalization12 certainly counts as circumstantial evidence that Avigad’s goals are consistent with 2. and 3.
Circumstantial evidence with respect to Avigad’s goals is, however, irrelevant to the question of whether the quotation is militant in the context of Avigad’s article. The author himself apparently thinks it is not, so it’s only fair to accept that it was not his intention. But there’s stronger evidence against my earlier claim. I reread Avigad’s article several times, expecting to find the assertion that the continuing development of new methods of formalization — as in the Xena project or, more immediately, at the Hoskinson Center for Formal Mathematics — will relieve practicing mathematicians of the need to be “logically adept and sufficiently motivated” and will ultimately reduce the discrepancy between informal and formal proof. Such a claim could be seen as evidence for my characterization of the quotation as militant, especially if accompanied by an injunction to mathematicians to incorporate formalization as a practical as well as idealized norm, since there now is (or soon will be) no excuse not to. I have seen such arguments in print, and much of this newsletter is devoted to explaining how they misrepresent what mathematicians are doing to a degree that can’t be excused by referring to norm (N).
But upon rereading Avigad’s article I realize it says no such thing. Instead, its second half is largely occupied by his explanation of “some common features of mathematical practice” in the form of a “list of … strategies” that “do in fact contribute to robustness and reliability.” Avigad borrows his use of the word “robust” from mechanical engineering, where it refers to the ability of a machine to function to specification while tolerating the inevitable slight “defects in modeling and manufacturing” as well as deviations from ideal operating conditions; analogously, an informal proof can tolerate slight imprecision or even misstated lemmas if its construction is sufficiently robust.
If the standard view is correct, the informal proof still serves to indicate the existence of a formal derivation, without having to live up to the unreasonably high standard of being completely error free.
In the end, it seems that Avigad’s and Azzouni’s papers both aim to resolve the same conundrum, which is to reconcile the observed reliability (and “robustness”) of typical informal proofs with the “standard view” (i.e., the Central Dogma). In listing his “common features,” Avigad is exposing readers of Synthèse, primarily an audience of philosophers, to something that is more than a repertoire of rules of thumb: these are recognizable characteristics of the actual disciplinary13 norms with which he, as a mathematician, is familiar in a way that Azzouni, who is not a mathematician, may not be.
A mathematician doesn’t have to endorse or even care about the “standard view” to agree that Avigad’s list of “common features” deserves to be brought to the attention of philosophers. In his conclusion, Avigad returns to the standard view however; he points to his defense of the claim, that I first saw as “militant,” that
…the gap between informal proof and formal derivation is not a good reason to reject the latter as a normative standard of correctness for mathematical proof.
I believe that the gap, combined with the absence of evidence that mathematicians accept formal derivation as a “normative standard of correctness,” together justify rejecting this putative normative standard. But I can no longer justify my earlier characterization of this or anything else in Avigad’s 2020 article as “militant.” I have added a correction (footnote 2) to the entry on the Central Dogma, with an apology to Avigad.
My original intention was to review Avigad’s more recent article entitled “Varieties of Mathematical Understanding,” but I have run out of time as well as space, so that will have to wait.
Comments are welcome on the Mathematics without Apologies blog.
Added September 29, 2022: This has already been noticed by philosophers.
An exception should be allowed for philosophers pointing out where other philosophers have gone wrong, but no more than necessary to eliminate the danger of infinite regress.
Unless you limit yourself to tautologies; but then it’s hard to get published.
Review of Proof and Other Dilemmas by B. Gold and R. A. Simons, Notices of the AMS, 1583, December 2011.
“Why Do Informal Proofs Conform to Formal Norms?” Found. Sci. (2009) 14:9-26.
Nor has there been one for philosophers since the Catholic church lost the franchise. See Amir Alexander’s Infinitesimal for the church’s attempts to outlaw the development of calculus.
If I were a philosopher I would here be professing adherence to “naturalism” in philosophy of mathematics, which consists in taking what mathematicians actually do as starting point, rather than some idealized version of what they ought to be doing. But I would be acting in full awareness that what I am professing is wrong if I were a philosopher, so it’s just as well that’s not what I am.
In contrast, I understand that it is perfectly legitimate and not at all misguided for computer scientists to devote attention to formal proofs. The mistake is only to assume that this is relevant to “ordinary mathematical practice.”
Writing “I believe” is of course purely rhetorical; no reader of a philosophical paper, or of this newsletter, really wants to know what the author believes but rather what the author adduces in support of these beliefs.
I’ve switched the order of the sentences for clarity; I don’t think this alters the meaning.
who have yet to kick the habit of presuming they know better than mathematicians what we’re really doing, but who for the most part concede that seeking self-awareness would distract our profession from the limited tasks we do perform well.