Concepts of Proof in Mathematics, Philosophy, and Computer Science

What a gift it was for me to be an undergraduate at UCLA in the 1970s! At the time the program in Mathematics was flexible to a degree that I cannot imagine can be matched today, with many pedagogical initiatives in place in our educational establishment. I look back at my days in Westwood over forty years ago and recall a prevailing laissez faire atmosphere (modulo the Darwinian constraint: you were certainly at liberty to flounder, and needed to be mathematically fit to survive). It was possible, if you knew how to finesse the system, to sample everything under the mathematical sun: a huge department even then, staffed with outstanding faculty including zealous researchers among the juniors, made for a smörgåsbord of courses and seminars.

Early on (in fact my first year there) I was captivated by the jazzy lecturing style and informality of a recent student of Robert Solovay, the late Telis Menas, who had a light touch in presenting deep themes in mathematical logic. I immediately enrolled in the three quarter sequence in logic and set theory, wherein Menas used a then brand-new text by Herbert Enderton, whose office was, as I recall, “upstairs.” Indeed, the upper floor of the Mathematics Building (and there were four very long meandering floors plus sporadic other offices on other floors) housed among others Donald (a.k.a. Tony) Martin and Yannis Moschovakis, very major players in logic and set theory. It was certainly in the air everywhere, as was everything else imaginable, of course. And there was a spirit of ecumenism in the land, extending to a lot of shared activity with the department of Philosophy across campus (i.e. across town: UCLA has always been an academic behemoth).

It was even the case that an undeniable living legend moved back-and-forth between these geographical extremes: Alonzo Church had a dual appointment in Mathematics and Philosophy and although he had made Dodd Hall (Philosophy) his headquarters on the North Campus, and taught his courses there, he occasionally made it to our neck of the woods on the South Campus. So the fix was in: UCLA was one of the best places to be for this interface between mathematics and logic. I, for one, spent a lot of time in the indicated courses and seminars (including one with Church himself) and even kept a taste for the subject through my graduate school years studying number theory (a seminar in recursion theory, just for fun), and even afterward: I am my department’s go-to instructor for kids who develop an interest in something from logic or set theory. And it’s always been very interesting.

Well, all this reminiscing serves as more than just self-indulgence in my early 60s: it is meant to give an indication why two of the three fields mentioned in the title of the book under review resonate with me in spades. I must admit, however, that it’s only two out of three, since computer science (other than in the abstract sense of formal languages and maybe Turing machines) is utterly alien to me, and has been so from the start. I am ornery enough to subscribe, still, to Halmos’s quip that “computers are important, but not to mathematics,” even as I know that I will be contradicted energetically by almost everyone these days.

What about the concepts of proof in these disciplines, then? Let me hint at the answer by citing three representative titles from this compendium of scholarly articles. The first one that strikes me as the sort of thing that should float the boat of any mathematician with even a quark of culture is Douglas S. Bridges’ “The continuum hypothesis implies excluded middle.” Here’s the abstract: “Within the framework of Bishop-style constructive mathematics, it is first proved that the Continuum Hypothesis (CH) implies the law of the excluded middle. A more explicit Brouwerian counterexample to CH is then discussed.” This is hot stuff right off the bat: Errett Bishop’s constructivism is contrasted with L. E. J. Brouwer’s intuitionism and we end up with radically different situations. And manifestly Bridges scores on both philosophical and mathematical counts with his focus on Aristotle’s tertium non datur.

Next, consider the article that precedes that of Bridges, namely, “Logic for Gray-code computation,” by Berger, Miyamoto, Schwichtenberg, and Tsuiki. It turns out that Tsuiki “introduced Gray code to the field of real number computation… [assigning] to each real number an infinite sequence [made up from three symbols, \(-1\), \(1\), and something denoting undefinedness] containing at most one copy of [the symbol for undefinedness].” Against this backdrop the authors “extract real number algorithms from proofs in an appropriate formal theory involving inductive and coinductive definitions.” I guess (taking the risk of offering an evaluation as a distant outsider) that we are dealing here with theoretical computer science with a vengeance, given that the notion of all real numbers is alien to finite state automata. Of course one can also observe that given any such automaton, i.e. any real world computer, it is trivial to produce already a mere rational number that is beyond its storing capacity. But this may be neither here nor there and I’m probably talking out of the back of my neck.

Finally let me mention the article by Jan von Plato (and can there be a better name for the author of “Aristotle’s deductive logic: a proof theoretic study”?). From the abstract: “Aristotle’s deductive logic, as presented in his book Prior Analytics, is a system of rules of proof. The structure of derivations by these rules is analyzed. It is shown that derivations can be so transformed that steps of indirect proof are applied at most once as a last rule, the only way in which Aristotle used indirect proof.” This, I think, is fabulous, and in fact conveys a sense of what is meant by “concept of proof in philosophy” as far as this book is concerned. Even though St. Thomas Aquinas famously referred to Aristotle as the philosopher, the latter’s philosophy as represented in the present book is more along the lines of the Analytics than, say, the Metaphysics, Poetics, or (Nicomachean) Ethics. Fair enough.

Obviously the book is quite specialized, and is pitched at a high (even professional) level. On the other hand a few things in the book are evocative to just about everyone; consider, e.g., the following statement on p.348 (in M. Rathjen’s article, “Remarks on Barr’s Theorem: proofs in geometric theories”): “If T is a geometric theory and A is a geometric statement deducible from T with classical logic, then A is also deducible from T with intuitionistic logic …” After all these years a statement like this still hits the mark for me, and I presume for many others. 

Michael Berg is Professor of Mathematics at Loyola Marymount University in Los Angeles, CA.