Computers, Justification, and Mathematical Knowledge

See Detlefsen and Luker (1980) and Teller (1980) for some replies.

Strict finitists and adherents of other extreme forms of constructivism might take issue with that, but we will subscribe to what has been the received view ever since Cantor and endorse the existence of infinitely many mathematical objects of various types, including proofs. To the extent that it is possible, we will try not to let this prejudge any epistemological questions, particularly in connection with aprioricity.

Burge(1998) and others have expressed similar positions, and we owe a debt to them, but our analysis here will take a different route.

In “a mixture of penitence and intransigence,” Kitcher has more recently revised his earlier account (2000), but continues to maintain that mathematical knowledge cannot be a priori, and that any philosophically interesting account of aprioricity must entail infallibility and indefesability.

In the present paper, when we speak of the proposition established by a proof we will mean the conditional proposition to the effect that the premises entail the conclusion. Whether or not the premises are known a priori is another question. We believe that quite a few mathematical truths can be known a priori by direct rational insight instead of inference (Peano’s axioms, for example), even though some others (such as certain set-theoretic axioms) might not be so knowable.

We assume that proofs are expressed in a sufficiently expressive formal system, and that there is a simple proof-checking algorithm that can be used to verify such proofs. That is the case, e.g., for first-order logic and for several higher-order type theories.

Some have expressed puzzlement as to how a proof can be unsound. In the words of Rota (1997, p. 183). “The expression ‘correct proof’ is redundant. Mathematical proof does not admit degrees. A sequence of steps in an argument is either a proof, or else it is gibberish.” However, the expression ‘correct proof’ is no more redundant than the expression ‘correct computer program’. Both proofs and programs have rich, recursive syntactic structure (a fact that is obscured in the preceding passage, which suggests that proofs are linear sequences of steps). Both can be given inputs and evaluated, and the evaluation can generate an error, or it can generate an output (in the case of proofs, the output is the conclusion). Correctness is always relative to specification. A proof can perfectly correctly derive a conclusion C ₁, but we might still call it incorrect if we expected it to derive some other conclusion C ₂ instead. Moreover, even if it does derive the desired conclusion, the question is what assumptions it requires in order to do so. A proof could correctly generate a conclusion with respect to one set of assumptions and fail with respect to others. Sets of assumptions are the primary “inputs” to proofs. This view of proofs as complex syntactic objects with formal evaluation semantics over assumption bases is developed at length by Arkoudas (2000). In this paper, by a “proof” D we will generally mean a syntactic object, essentially an abstract syntax tree (AST) in some appropriate abstract grammar (Reynolds 1998). We will be quite liberal on what counts as a token \({\widehat{D}}\) of such a proof D; it could be either (a token of) a linear string over some alphabet that can be parsed into an AST, or (a token of) a two-dimensional picture of an AST, and so on. If a token \({\widehat{D}}\) is incorrectly mutated, then the resulting physical object might fail to be a token of any proof, or it might become a token of some other proof. Precise identity criteria for proofs can be given but need not concern us here.

Such facts will include both specific observations and generalizations, e.g., an assertion to the effect that humans can reliably carry out algorithms.

These are, of course, very similar to the idealizations made by Turing in his analysis of computation. An important difference is that Turing did not require any understanding beyond the ability to follow rules.

There are some subtle issues here. If we require direct understanding of a proposition P in order for P to be known, then propositions expressed by very large formulas cannot be known at all—and a fortiori cannot be known a priori—by an ordinary person, even one who is equipped with unbounded time, paper, ink, and patience (although they could be known by persons with arbitrarily—but finitely—larger intellectual capacities than ours). Even instances of tautologies such as x =  x would be unknowable for sufficiently large values of x, such assince we cannot directly comprehend the proposition expressed by such a formula. However, ordinary persons can know a proposition indirectly, by description, as in “the proposition expressed by (3)” or “the proposition established by the proof I just checked,” provided we know that such definite descriptions designate unique propositions, and in that sense arbitrarily large proofs can indeed provide knowledge.

Of course one need not subscribe to functionalism (neither author does) in order to recognize the multiple realizability of algorithms.

However, see Rapaport (1999) for an alternative account of implementation.

That is, apart from error messages.

This simply means that there is an algorithm for listing all and only the theorems of the system. We do not wish to consider, for instance, systems with uncomputable inference rules, and the recursive enumerability proviso blocks such systems.

Some philosophers (Williams 1972) have denied that mathematical knowledge can ever result from testimony. Most hold that reliable testimony produces a posteriori knowledge. Burge (1993) has tendentiously argued that not only can one come to know a mathematical proposition via someone else’s testimony, but can come to do so a priori. Burge’s arguments are subtle and deserve careful attention, but his position is prima facie implausible.

Quoted by MacKenzie (1999, pp. 46–47), who provides an interesting sociological discussion of the four-color theorem.

Of course we also need to believe that the semantics are right, that the system is consistent, and so on. But the deeper we go the more conceptual the issues become, and the less they have to do with the role of computers.

The ideas were already there, but implementations were not powerful enough.

Personal communication, January 22, 2006.