“Why Do We Believe Theorems?,” A. Pelc (2009)

I recently posted a paper discussing economists’ distaste for simulation-based results. An important part of that argument is that writing down formal proofs has value beyond simply the results of the proof – it lets us understand our intuition at a deeper level, it makes clear the mathematical, and therefore economic, connections between different lines of research, etc. But there is a more fundamental question about proofs which has been studied by philosophers of mathematics at least since Hilbert: why should we believe proofs?

Here, I don’t mean, why should we believe that proofs in economic theory have anything to do with the real world. Rather, I (and Pelc, in this recent paper in Philosophia Mathematica) mean that proofs, as written, are rarely constructed from first principles. Assume that some fancy new result in decision theory, with ten pages of topology in the appendix, is (implicitly) proven using the axioms of some well-defined axiomatic system like Peano arithmetic or ZFC set theory. Ignore for now whether you think the particular implicit axioms are OK – I worry about the Axiom of Choice myself, and one of my classmates here refuses on philosophical grounds to use proofs by contradiction. Formalism in mathematics is essentially a modification of Hilbert’s Second Question: if a statement is undecidable (that is, if we can prove it in a formal axiomatic system), then the proof is convincing because we can reduce the proof to logical statements about axioms and check the proof mechanically.

Now, nobody actually writes down a full derivation from axioms of everything they prove – that would be incredibly boring, tedious, and useless. Rather, a proof is a set of statements like A implies B implies C. If it’s not clear how A implies B, we can write A implies A1 implies A2 implies A3 implies B, for instance. But then, some reader might not find A2 implies A3 convincing, and we’ll need to write A2 implies A’ implies A3. The important point is that the detail needed for a proof to be convincing is not inherent in the proof; it depends on the reader. For a sufficiently complicated proof, the amount of detail needed to convince every reader that we could, in theory, write the proof down as a derivation from axioms has no obvious upper bound in the number of logical statements necessary. Because of this, Pelc argues, it is not even clear that proofs can be reduced to derivations and checked using a mechanical proof checker, even in theory, since Planck time and the span of the universe limit the number of logical statements we could conceivably check.

The upshot of all this is that the reasons sufficiently complex proofs are believable – meaning accepted universally as “true” within a given system by basically all mathematicians – cannot be for a formalist, Hilbert-style reason. Rather, the universal acceptability comes from more prosaic reasons – semiotics, common nonformal meanings of terms accepted within a community, etc. – which you might associate with philosophies far from the analytic school. For economists, this means that using mathematics as a language to formalize proofs does not necessarily allow us to claim that results are “true by logic” or anything so strong, even if we accept the required axioms as true (or at least “true” with the context of the paper); there’s simply no way to avoid some sense of group subjectivity in science, even one as seemingly hard as mathematics.

http://philmat.oxfordjournals.org/content/17/1/84.full.pdf+html (Final version, ungated as of the day of posting. This essay appeared in the “Best of Mathematical Writing 2010” which was linked to recently by RJ Lipton)

Advertisement