- 1 There are, for example, over two hundred proofs of the law of quadratic reciprocity, all aimed at a (...)
- 2 This question is different from, and I will suggest prior to, questions regarding the nature of mat (...)
1In their practice mathematicians prove, and reprove, theorems—in some cases hundreds of times1—in order better to understand. But how does the practice of proving theorems result in mathematical understanding? What is a proof that it yields understanding (when it does)? These questions are all the more difficult insofar as a proof as it is conceived in mathematical logic, as a formal derivation of a theorem from axioms, seems to have nothing whatever to do with understanding. Is perhaps the locus of mathematical understanding something other than proof? Or should we perhaps think instead that mathematicians' proofs are something essentially different from derivations as they are understood in mathematical logic? What exactly is the relationship between, on the one hand, the mathematical practice of proving theorems, and on the other, the desired mathematical result of better understanding?2
2Needless to say, no fully adequate answer can be provided here. What I aim to do is, first, to identify what I take to be the most fundamental issue regarding proof and understanding in mathematical practice, the issue that must be addressed before anything more detailed can be said about how particular proofs, or particular sorts of proofs, enable understanding, or about the nature of mathematical understanding, or about different aspects of the mathematician's understanding. As developed in the first section, the problem is that given our current conception of formal proof it is impossible to see how such a proof could possibly advance our understanding because a formal proof abstracts from all content. But if that is right then we need to reconsider the notions of formal reasoning and formal proof. In the second section two quite different accounts of what one might mean by formal reasoning are outlined, one in which form is fundamentally opposed to content and one in which it is not. In the third section I turn to the sort of algebraic reasoning that was the norm in mathematics in the eighteenth century in order to clarify the idea that one might reason in a way that is at once fully rigorous, and hence in a sense formal, and also from the contents of mathematical ideas. In Section
3Four some ideas are very briefly sketched regarding how one might extrapolate from that case to the sort of mathematical reasoning that since the nineteenth century has been the norm in mathematical practice. The fifth section concludes the discussion.
- 3 This is not the only conception of proof and logic in circulation. It nonetheless is very standard (...)
4According to what it seems fair to say is the standard view, a mathematician's proof is a sequence of sentences beginning with axioms each subsequent sentence of which is a logical consequence, in the technical sense due to Tarski, of an earlier sentence or sentences.3 Suppes Introduction to Logic, published in 1957, is a classic exposition of the view. First, it provides "a completely explicit theory of inference adequate to deal with all the standard examples of deductive reasoning in mathematics" [Suppes 1957, xii]. The underlying idea of this explicit theory is of course very familiar, but it is worth rehearsing nonetheless. On this view:
A correct piece of reasoning, whether in mathematics, physics, or casual conversation, is valid in virtue of its logical form. Because most arguments are expressed in ordinary language with the addition of a few technical symbols particular to the discipline at hand, the logical form of the argument is not transparent. Fortunately, this logical structure may be laid bare by isolating a small number of key words and phrases like 'and , 'not , 'every , and 'some . In order to fix upon these central expressions and to lay down explicit rules of inference depending on their occurrence, one of our first steps shall be to introduce logical symbols for them. With the aid of these symbols it is relatively easy to state and apply rules of valid inference. [Suppes 1957, xii]
5Once having mastered translations into the symbolic notation and the rules governing inferences involving the logical signs in the system (Chapters 1-6), the student is equipped to navigate the differences between a formal proof and an informal proof of the sort, it is claimed, that mathematicians in their practice actually provide (Chapter 7). On the account Suppes outlines, whereas the mathematician's (informal) proof has jumps in the deductive reasoning, in a fully formalized proof all the jumps have been replaced by small steps that are manifestly instances of the rules of formal logic. "In giving an informal proof, we try to cover the essential, unfamiliar, unobvious steps and omit the trivial and routine inferences". A formal proof includes even the trivial and routine inferences [Suppes 1957, 128].
- 4 See especially Chapter 7. See also Yehuda Rav's critique of the view in [Rav
6But as has been more recently noted, this seems, surprisingly, not to be right. Mathematicians, in their actual practice, often do not give proofs in this sense; they do not set out a chain of deductions, whether or not with jumps in the reasoning. Instead, they describe how the chain of reasoning goes, or would go if one actually engaged in it. As Bostock has put the point, in mathematical practice "one does not actually construct such proofs [i.e., fully formalized, or even gappy, deductive proofs from axioms]; rather one proves that there is a proof as originally defined" [Bostock 1997, 239]. Avigad similarly suggests that "real" proofs, that is, the proofs that mathematicians actually give, "are simply higher-level, informal texts that indicate the existence of lower-level formal ones; i.e., they are recipes, or descriptions" [Avigad 2006, 132]. This feature of the proofs that mathematicians actually provide is the basis also of Azzouni's "derivation-indicator view of mathematical practice" [Azzouni 2006].4 As Azzouni sees, what the mathematician provides is only something that indicates that there is a derivation; what is given is not the derivation itself, that is, the chain of reasoning (whether or not with gaps or jumps) from one claim to another according to rules of valid inference. Now Azzouni does think, as does Avigad, that the derivation itself, the derivation that is only described by the mathematician, can be given in the symbolism of standard mathematical logic, and that, we will see, may not be so. But I want for the moment to leave this to one side in order to focus more closely on the idea that mathematicians proofs are in fact not proofs in the sense of chains of reasoning but instead descriptions of such proofs.
- 5 It should not be inferred that the distinction has a sharp boundary; there are intermediate and mix (...)
7A simple example illustrates the difference we are concerned with here.5 Suppose you are given the task of dividing eight hundred and seventy-three by seventeen. You might solve the problem by engaging in a bit of mental arithmetic that you could report as follows.
A hundred seventeens is seventeen hundred; so fifty seventeens is half that, eight hundred and fifty. Add one more seventeen—so that now we have fifty-one seventeens—to give eight hundred and sixty-seven. This is six less than eight hundred and seventy-three. So the answer is fifty-one with six remainder. Alternatively, you might do (or imagine doing) a standard paper-and-pencil calculation in Arabic numeration the result of which (if you were schooled in North America) will look something like this:
- 6 More exactly, we have a trace left after the paper-and-pencil activity of reasoning has been comple (...)
8Either way, one gets the answer that is wanted. But the two collections of marks serve very different purposes. The written English, it seems fair to say, provides a description of some reasoning, in particular a description of the steps of mental arithmetic a person might go through in order to find the answer to the problem that was posed. The description does not give those steps themselves. To say or write that a hundred seventeens is seventeen hundred is not to calculate a product. Even more obviously, to say or write the words 'add one more seventeen' is not to add one more seventeen. It is to instruct a hearer or reader: at this point in their reasoning, assuming they are following the instructions, they are to add seventeen. The paper-and-pencil calculation is radically different. It is manifestly not a description of a chain of reasoning one might undertake; rather it shows a calculation—at least it does so to one familiar with this use of signs to divide one number by another. (Notice that the paper-and-pencil calculation does not show the steps that are described in the first passage; calculating in Arabic numeration does not merely reproduce mental arithmetic but involves its own style of computing.) Working through this collection of signs in Arabic numeration, or performing the calculation from scratch for oneself, just is to calculate. Here we have not a description of reasoning but instead a display of reasoning.6 One calculates in the system of Arabic numeration in a way that is simply impossible in natural language. To one who is literate in this use of the system of written signs, the calculation shows the reasoning.
- 7 The list is due to Avigad, [Avigad 2006, 131].
9Bostock, Avigad, and Azzouni all claim that proofs in contemporary mathematical practice describe rather than display the reasoning. This is easily verified by looking at the form of expression of the proofs that are provided in standard contemporary textbooks of college level mathematics, say, in abstract algebra. The following descriptive phrases, taken from proofs in the opening chapter of Birkhoff and Mac Lane's classic A Survey of Modern Algebra (1965), are typical:7
-… the first law may be proved by induction on n.
- ... by successive applications of the definition, the associative law, the induction assumption, and the definition again.
- By choice of m, P (k) will be true for all k < m.
- Hence, by the well-ordering postulate ...
- From this formula it is clear that ...
- This reduction can be repeated on b and r1 ...
- This can be done by expressing the successive remainders ri in terms of a and b ...
- By the definition of a prime...
- On multiplying through by b ...
- ... by the second induction principle, we can assume P (b) and P (c) to be true ...
- Continue this process until no primes are left on one side of the resulting equation ...
- Collecting these occurrences, ...
- By definition, the hypothesis states that ...
- … Theorem 10 allows us to conclude ...
10Proofs written using such phrases are not themselves the reasoning but instead accounts of how the reasoning is to go and would go were one actually to reason from the starting point to the desired theorem. They tell you what to do rather than showing you the doing of it.
- 8 The list is due to Freek Wiedijk in [Wiedijk 2008, 1408].
11Mathematicians in their practice do not give formal, or even formalizable— in Suppes' sense of filling in all the gaps in the reasoning—proofs but instead only describe chains of reasoning. We need, then, to ask whether the chains of reasoning that the mathematician describes can be formalized in Suppes sense. In one respect the answer is obviously yes. We do know how to take a mathematician's proof and on that basis produce a fully formalized proof, and have actually done this for various mathematically significant proofs— among them, Gôdel's first incompleteness theorem, the Jordan curve theorem, the prime number theorem, and the four-color theorem.8 But what exactly is the relationship between the mathematician's reasoning and the formalized proof? The answer is not obvious and it is not obvious because a formalized proof is usually unintelligible. A formalized proof does not provide or even advance mathematical understanding. There are only two options. If we as sume that the formalized proof does set out the chain of reasoning that the mathematician describes, it would seem then to follow, in light of the fact that the formalized proof does not advance understanding, that mathematical understanding does not reside in the practice of proving theorems but instead in some other aspect of mathematical practice. Alternatively, one might argue that the formalized proof does not set out the mathematician's reasoning, the reasoning that is described in a textbook proof, precisely because a mathematician's chain of reasoning—the reasoning that is described in a textbook proof—can advance one's mathematical understanding. On this second approach, one begins with the thought that the mathematician's reasoning does, at least in some cases, advance mathematical understanding. But because we know that the corresponding formal proof does not advance mathematical understanding, one concludes that the mathematician's reasoning cannot be identified with a formal proof.
12Manders embraces the first horn. He accepts the mathematical logician's formal conception of proof but then locates mathematical understanding out-side of proof, in the conceptual settings (as he calls them) of proofs. And he does so because, he sees, the reliability that is gained in formalizing a proof is achieved at the expense of understanding: "fully formalized proofs are usually unintelligible. Whatever goes into clarity of mathematical ideas can be obscured by the way those ideas are represented in reliability theoretic mathematical foundations" [Manders 1987, 202]. For Manders, because he assumes that questions of reliability are adequately settled by formalizing proofs, while at the same time recognizing that formalization is inimical to understanding, it simply cannot be the case that the locus of mathematical understanding is proof.
- 9 See also [Goethe & Friend 2010].
13Rav argues contrapositively that because a mathematician's proof can provide mathematical understanding, the mathematician's reasoning cannot be identified with a formalization. Although, Rav thinks, "most of our current mathematical theories can be expressed in first-order set-theoretical language", a mathematician's proof cannot be formalized because it "depends on an understanding and prior assimilation of the meanings of concepts from which certain properties follow logically" [Rav 1999, 20, fn 20, and 29]. A mathematician's proof, Rav argues, is irreducibly meaningful; it has irreducible semantic content and so cannot be identified with a derivation in some formal system precisely because such a derivation is merely syntactic.9
- 10 Of course, creative mathematicians use a variety of non-deductive methods in formulating plausible (...)
14As the arguments of Rav and Manders taken together indicate, the conception of formal proof that we inherit from mathematical logic leaves us with only two choices: either a mathematician's proof is (or at least can be) a source of mathematical understanding and is essentially different from a formalization of it, or the mathematician's proofs are formal, that is, in principle formalizable, but are not the means by which one achieves mathematical understanding. I think that we should be very puzzled by this. Surely our logic is, just as Suppes says, "a completely explicit theory of inference adequate to deal with all the standard examples of deductive reasoning in mathematics" [Suppes 1957, xii]. It is barely conceivable that the norms governing the reasoning mathematicians actually engage in are simply disjoint from the familiar rules of logical inference.10 But if so, then why is it that conceptual clarity in mathematics is essentially different from formal clarity? This is the problem of proof and understanding that we are concerned with here.
- 11 Koen Vervloesem also makes this point in his discussion of the difference between human and compute (...)
15Manders and Rav agree that a fully formalized proof has nothing whatever to do with mathematical understanding. And it is not hard to see why it does not: a fully formalized proof does not depend in any way on content or meaning. In a formal proof what matters is not (non-logical) content but only the logical particles in virtue of which the rules governing permissible moves may be applied. One does not have to think at all about what is being claimed or inferred in a formal proof, as is made manifest in the fact that such proofs are machine-checkable. Indeed, this is a large part of the point of the formalization; the point is to make any and all relations of meaning explicit, all steps in the proof purely syntactic, so that one can see precisely on what the proof depends. But there is a puzzle hidden here. A proof, Rav suggests, has irreducible semantic content. Mathematicians, if he is right, reason on the basis of contentful mathematical ideas. Thurston, a practicing mathematician and Fields medalist, concurs: "reliability does not primarily come from mathematicians formally checking formal arguments; it comes from mathematicians thinking carefully and critically about mathematical ideas" [Thurston 1994, 47]. Thurston, unlike Rav, does think that (at least in a sense) mathematicians proofs can in principle be formalized. "However", he cautions, "we should recognize that the humanly understandable and humanly checkable proofs we actually do are what is most important to us, and that they are very different from formal proofs" [Thurston 1994, 48]11 But supposing that mathematicians do reason on the basis of contentful mathematical ideas, then we should be able to make those ideas, and the steps of reasoning they enable, explicit so as to see precisely on what the reasoning depends, and we should be able to do that without losing sight of meaning altogether. But it is just this that we seem not to be able to do insofar as properly logical, rigorous reasoning depends, we think, on form as contrasted with content. Hence, to make the mathematician's reasoning fully explicit is to show that it does not, after all, rely on any meanings, any semantic content, but only logical form.
16On the model-theoretic account of logic and language that is due to Tarski, a language involves two essentially different and opposed elements, logical form, which alone matters to the goodness of inference, and content that is given by an interpretation or model. More exactly, on this conception, a (first-order) language involves four essentially different sorts of signs that following Hodges we can characterize as follows:
First, there are the truth-functional connectives. These have fixed logical meanings. Second there are the individual variables. These have no meaning. When they occur free, they mark a place where an object can be named; when bound they are part of the machinery of quantification.. . The third symbols are the non-logical constants. These are the relation, function, and individual constant symbols. Different first-order languages have different stocks of these symbols. In themselves they don t refer to any particular relations, functions or individuals, but we can give them references by applying the language to a particular structure or situation. And fourth there are the quantifier symbols. These always mean 'for all individuals' and 'for some individuals'; but what counts as an individual depends on how we apply the language. To understand them, we have to supply a domain of quantification. The result is that a sentence of a first-order language isn't true or false outright. It only becomes true or false when we have interpreted the non-logical constants and the quantifiers. [Hodges 1985/6, 144]
17On this conception, what matters to the goodness of inference is only logical form. An inference from some premise or premises P to a conclusion C is good just in case C is a logical consequence of P, that is, there is no interpretation or model in which P comes out true and C false. To have a fully rigorous chain of reasoning is thus to dispense with all content and meaning, to attend only to form. To reason rigorously, on this account, is to be impervious to extra-logical meanings.
18To reason rigorously is to make everything on which one's reasoning depends explicit; it is to state in advance all the premises and assumptions that are required in the derivation of the conclusion. Tarskian model theory commits us to something stronger, to the idea that meanings have nothing at all to do with the goodness of inference. The notion of logical consequence reduces an act of inference, the derivation of some conclusion from a premise or premises, to a purely formal, syntactic relation between uninterpreted strings of signs. And although the demand for rigor, for a formal proof in that sense, does not require that one strip all meaning from one's non-logical constants but only make all assumptions explicit, the step from the demand for rigor to the requirement that one formalize one's chain of reasoning in some mean-ingless system of signs has seemed to many a short one indeed. We read, for instance, in Nagel's classic essay "The Formation of Modern Conceptions of Formal Logic in the Development of Geometry":
Everyone is aware, he [Pasch] pointed out, of the dangers which threaten the geometer who uses diagrams and other sensory images; but few seem to be equally aware of the traps which we lay for ourselves when we employ common words to designate mathematical concepts. For such words have many associated meanings not relevant to the task of a rigorously deductive science, and those associated meanings sway us to the detriment of rigor.
[Nagel 1939, 238]
19So far, so good, one might say: it is for just this reason that we need elucidations of our primitive signs, explicit definitions of other terms, axioms setting out the basic truths of the system, and rules on the basis of which alone anything can be derived. Nagel, however, continues:
To avoid these handicaps it is therefore desirable to formalize the set of nuclear propositions; that is, we ought to replace them by a series of expressions in which the "geometrical concepts" of the propositions have been replaced by arbitrarily selected marks, whose sole function is to serve as "places" or blanks to be filled in as occasion may warrant. The result of such a formalization is an "empty frame", which expresses the structure of the set of nuclear propositions and which is alone relevant to the task of pure geometry.
20In pure geometry, according to Nagel, all meaningful words, that is, all non-logical words, are to be replaced by meaningless symbols to ensure that one draws no inferences that are grounded in meaning. Pure geometry, like pure mathematics generally, is to be conceived (on this view) as the manipulation of empty marks according to rules.
21But, again, rigor does not entail formalism in this sense. All that rigor requires is that no steps are to be made in the system save those permitted by the axioms, definitions, and given rules of inference, which serves to ensure that all one's presuppositions have been made explicit. Although it is true that the possibility of following the rules mechanically, as if one's non-logical primitive signs had no meaning, can serve as a test of the adequacy of one's system of axioms and definitions, it simply does not follow that one should conceive one's signs as empty of all meaning and signification. As Frege puts the point, "it is possible, of course, to operate with figures mechanically, just as it is possible to speak like a parrot. . . [But] it only becomes possible [to do this] after the mathematical notation has, as a result of genuine thought, been so developed that it does the thinking for us, so to speak" [Frege 1884, iv]. "The use of symbols must not be equated with a thoughtless, mechanical procedure. . . One can think also in symbols" [Frege 1976, 33]. If Frege is right, mathematicians develop systems of written signs not to dispense with all content but instead to express content in a way that enables rigorous reasoning on the basis of that content.
22Why then does Nagel so easily slide from the demand for rigor (for a formal proof in that sense) to the demand for formalization in his sense? Why does he think that the only way to avoid being "swayed" by "associated meanings" is by jettisoning meanings altogether? A plausible answer, or at least part of an answer, is that he associates rigor with mechanism: to be really rigorous is to think like a machine, impervious not only to associated meanings but to any meaning at all.
23Mathematicians in their practice do not think like machines any more than chess masters play chess merely mechanically, that is, as chess-playing computers do, by brute number crunching (hundreds of millions of moves per second). Nevertheless, it can seem that the goodness of inference really does rely only on logical form as contrasted with content. In fact this is not so. Although there is a perfectly good sense in which inferences are valid in virtue of their form, it does not follow that the notion of logical form fundamentally contrasts with and is opposed to that of semantic content, of content as it matters to understanding and truth. It is perfectly possible to accept that inferences are valid in virtue of their form while rejecting the distinction between logical form and content that is codified in the model-theoretic conception of language that we find in mathematical logic. For to say that an inference is valid in virtue of form need mean no more than that the inference is an instance or application of something more general, a schema or rule that applies not only in the given case but also in other cases that are relevantly like it.
24Consider, for example, the (material) inference from 'Felix is a cat to 'Felix is a mammal . This inference is good, if it is good, because one can infer generally from something's being a cat that it is a mammal; the inference is good (if it is good) because inferences of the form 'x is a cat; therefore, x is a mammal' are good. The inference is not good in virtue of being about Felix. Though one does infer something about Felix, the validity of the inference is explained not by reference to Felix but by appeal to a rule, something to the effect that being a cat entails being a mammal. Similarly, the inference from John is in the kitchen or the den' and John is not in the den' to John is in the kitchen' is good, if it is good, because one can infer generally from something's being this or that, and its not being that, to its being this. The inference is not good in virtue of being about John's whereabouts. Though one does infer something about John's whereabouts, the validity of the inference is explained not by reference to John but by appeal to a rule, namely, the rule we call disjunctive syllogism. Whereas in our Felix example the rule concerns valid inferences that rely on the meanings of the words cat' and mammal', in the John example the rule concerns valid inferences that rely on the meanings of the words or' and not'. And just the same is true in all other cases of actual inference, whether material or formal; any actual inference is an instance of a rule that applies also in other cases.
25The model-theoretic conception of language according to which logical form stands opposed to semantic content commits us to something stronger. It commits us, first, to the idea that the Felix inference is not really a valid inference at all. On this view, no inference is valid in virtue of meaning, from which it follows directly that 'cat' and 'mammal' play an essentially different role in reasoning from words such as not' and or'. Somehow, on this view, logical contents such as that given by or' and not' are not really contents, meanings, at all but only forms, or form indicators.
26Particular contents, at least as contents are understood on the model-theoretic view, do not matter to the validity of an inference or of a chain of inferences in a proof. But, we have seen, particular contents do seem to matter in mathematical reasoning. Though any inference is valid in virtue of its form, actual mathematical reasoning is reasoning from the contents of concepts, from mathematical ideas. Even so much as to begin to understand how this can be, we need to bear in mind that although there is a clear sense in which inferences are valid in virtue of their form (because they are instances of something more general), it does not follow that language should be conceived model theoretically, in terms of a thoroughgoing distinction between logical form and content as it matters to meaning, understanding, and truth.
27Mathematicians, in their practice, reason on the basis of content. But because we tend to think that logical form is opposed to content, that the goodness of inference is independent of content, the notion of a fully formalized mathematical proof generates a philosophical difficulty. It becomes impossible to understand how a mathematical proof could further mathematical understanding. Either a mathematical proof can advance one's mathematical understanding, in which case it cannot be identified with a fully formalized proof, or it can be fully formalized, made machine checkable, but does not contribute to mathematical understanding. The problem here is clearly not with the very idea of rigor. It is perfectly coherent that one might reason fully rigorously on the basis of content. The problem is that we do not know how to make intelligible the idea of reasoning on the basis of content, mathematical ideas. It is to this problem that we now turn.
28We have seen that our standard way of thinking about logic (and language) makes it very hard to see how reasoning might be on the basis of content. I want, then, to set that standard way of thinking aside as far as possible and consider instead the sort of constructive algebraic problem solving that was characteristic of mathematical practice in the eighteenth century, long before we had anything even approaching our contemporary views of logic. Such problem solving is done in the familiar symbolic language of algebra that we all learned as school children and as is well known, it can be made fully rigorous in an axiomatization. As I will argue, this language, together with the mathematical practice that uses it, provides, at least on one plausible interpretation, an illustration of how one might reason on the basis of content in mathematics.
29Among the axioms of elementary algebra are these:
1. a + b = b + a
2. (a + b) + c = a + (b + c)
3. a x b = b x a
4. (a x b) x c = a x (b x c)
5. a x (b + c) = (a x b) + (a x c).
- 12 Warren Goldfarb rehearses some of the history [Goldfarb 1979].
30Given these axioms governing permissible rewritings, one can further derive various theorems, which similarly govern permissible rewritings, for instance, this: (a + b)2 = a2 + 2ab + b2. But how exactly should we think of these axioms? One way is quantificationally, that is, in terms of a conception of generality that was fully clarified only in the early decades of the twentieth century12 On this way of thinking, the axioms are implicitly universally quantified claims about numbers, basic truths about numbers, all of them. A second way, following Hilbert, is to think of them as implicitly defining addition and multiplication, as stipulations about what we will mean by the signs '+' and 'x'. The grounds for thinking of the axioms this way are familiar: although we can read the axioms as truths about numbers, as on the quantificational reading, those same axioms can also be interpreted very differently, as truths about quite different sorts of objects. So long as the axioms are satisfied in a given domain then the derived theorems will hold in that domain. And this is, of course, an important, and importantly mathematical, insight.
31But there is also a third way of thinking of these axioms. We can treat the axioms, and the theorems derived from them, neither as truths about numbers nor as uninterpreted stipulations for which many models might be given, but instead as basic and derived truths about the operations of addition and multiplication, as ascribing higher-level properties to those operations, in our axioms here, commutativity, associativity, and distribution. On this reading, the axioms and theorems are perfectly meaningful (as they are not on the second, Hilbertian reading), but they are in no way about numbers (as on the first, quantificational reading). What the axioms and theorems concern on this third reading are certain arithmetical operations and particular properties of those operations. On this reading, the axioms set out basic properties of those operations and on that basis one derives theorems that ascribe other, non-basic properties to those same operations.
- 13 The reading to be outlined was developed in comments by an anonymous referee of an earlier draft of (...)
32It is important that we be clear about what this third reading amounts to, and to that end it will help to consider an interpretation of it that does not capture what we are after here13 On the (mistaken) interpretation, the first axiom is fully expressed thus:
(∀a,b є N)( ∀ + є S)a + b = b + a.
- 14 It is perhaps at least worth noting that on this reading the letters 'a', 'b', and 'c' do not funct (...)
33The three readings outlined above are then to be taken to correspond to three different answers one might give to the question what is assumed to be fixed and what can vary in an interpretation. On the first, quantificational reading, both N and S are assumed fixed. On the second, Hilbertian reading, both N and S are treated as uninterpreted independent of the specification of a model in which the axiom comes out true. The third reading, on this account, keeps S fixed but allows N to vary with different interpretations. (And a fourth possibility opens up as well, namely, to keep N fixed and let S vary.) But that is not what is intended here. The third reading we are after, according to which the axioms ascribe properties to the operations of addition and multiplication, does not involve any quantifiers at all. It has the form of a simple predication; it is like an ascription of a property to an object, something of the form 'Fa', but is one level up insofar as the "object" in this case is the addition function (not the numbers that function correlates but the correlating function itself), and the property ascribed is a second-level one. To explain how exactly the notation would have to be functioning to serve this expressive purpose would take us too far afield14 For our purposes what is important is that such a reading is available, and that it is quite different both from the first quantificational reading and from the (related) Hilbertian reading. On the first reading the axioms are about some objects and ascribe properties and relations to those objects, all of them. On the second reading, the axioms are about some particular domain of objects only on an interpretation (in a model) that makes the axioms true. On the third reading, the axioms are not about objects, numbers, but about particular arithmeti-cal functions, and they ascribe various (higher-level) properties and relations to those arithmetical functions.
- 15 Of course in the order of knowing one first learns of particular pairs of numbers, say, seven and f (...)
34The third reading of the axioms (and theorems derived from them) as as-criptions of properties to the operations of addition and multiplication can help to clarify the first two readings as follows. First, if, as the third reading has it, addition has the property of being commutative, then it obviously follows that for any two particular numbers a and b, a + b = b + a. It follows, that is, that the quantificational reading of that same axiom is true. But now, as we can see, that universally quantified generality is not known to be true directly. How could it be given that there are infinitely, indeed, non-denumerably many numbers to which it applies? Instead that quantified generality is known to be true because the operation of addition has the property of being commutative.15 It is not merely an accidental truth about numbers that, as it happens for any two of them, the first plus the second is equal to the second plus the first. It is, rather, necessary that this be so. And this necessity at the level of individual, particular numbers can be explained by the fact, one level up—that is, at the level of operations on numbers rather than at the level of the numbers themselves—that the operation of addition has the property of being commutative.
35The second, Hilbertian reading is also explained because what the Hilbertian reading really reflects is the fact that inferences are valid in virtue of their form, the fact that they are instances of something essentially general that can be applied in other cases. The basic idea is this. If, as on our third reading, we take our axioms and theorems to be ascriptions of properties to the operations of addition and multiplication, then we can see as well that the inferences from the axioms to the theorems are not good in virtue of the fact that they are about addition and multiplication—any more than our inference about Felix was good in virtue of being about Felix. They are good because having those particular properties that are ascribed in the axioms entails having certain other properties as well. That is just what the derivations of the theorems from the axioms show. It follows directly that any other function or operation having the same particular properties as are ascribed in the axioms will also have the properties that are ascribed in the theorems that are derived from the axioms. The Hilbertian insight that the axioms and theorems can be applied in other cases does not show that the model-theoretic conception of language is the right conception to have. For that insight can be seen instead as a reflection of the fundamental feature of inference we have already remarked on, the fact that any particular inference is an instance or application of a general rule that can be applied also in relevant other cases.
36On our third reading, the axioms of elementary algebra are contentful truths about the addition and multiplication functions from which other truths follow. All these (basic and derived) truths function in turn to license inferences in particular cases. They can, in other words, be applied as rules in solving construction problems and in demonstrating theorems. Consider, for illustration, this theorem: if two numbers are each a sum of two integer squares then their product is also a sum of integer squares. In order to show algebraically that this theorem is true, we begin by formulating the starting point in the symbolic language. We have two numbers that are each a sum of two integer squares, which we express in the symbolic language thus: a2 + b2 and c2 + d2. What we must show is that their product is also a sum of integer squares. So we write down the product of our two sums thus: (a2 +b2)(c2 +d2). Notice what we have done here. We began with a certain mathematical idea, the idea, or as we can also say, the concept, of a sum of two integer squares. The content of that concept, what it is to be a sum of two integer squares, was then expressed in the language of algebra: a2 + b2. This expression, 'a2 + b2', does not merely abbreviate the English phrase—though one could imagine so using the signs (perhaps thus: + 212)—but instead formulates in a specially designed system of signs the content of that English phrase, what it means. To express the idea that we have two such sums we then used different letters in place of 'a' and 'b', and on that basis we were able to exhibit the content of the idea of a product of two numbers that are, each of them, a sum of two integer squares: (a2 + b2)(c2 + d2). Having thus formulated the content of the concept product of two sums of (two) integer squares in an arithmetically articulated complex of signs in the language, we can now apply the rules given in the axioms and derived theorems.
37Leaving out obvious steps—steps that we could easily put in, tedious thought it would be to do so—the fifth axiom licenses the move from
( a 2 + b2 )( c2 + d2 )
a2c2 + a2d2 + b2c2 + b2d2
Notice, first, that although the rule applies to a certain form of expression it is still perfectly possible to keep the content expressed in view as we apply the rule. As an indication of this we can express the rule in axiom 5 in (meaningful) words: if you have a product of a number and a sum then it can be rewritten as a sum of the products of the number together with each of the summands. It is also worth remarking that although we generally think of inferential articulation as something that involves a relation between concepts, here we are dealing with an internally articulated idea. It is the whole expression that sets out the idea with which we are concerned, that is, the idea of a product of two sums of integer squares, but because that expression is internally articulated, we can apply the rewrite rules of elementary algebra to it.
38Now we need to reorder to get:
a2c2 + b2d2 + a2d2 + b2c2
At this point a student might wonder why that was a good move to make. The reason, however, becomes clear at the next step in which we both add and subtract 2abcd (with the letters appropriately reordered) to give, after some reorganization,
a2c2 - 2acbd + b2d2 + a2d2 + 2adbc + b2c2.
And now even the student ought to be able to see that this last expression can be rewritten (by appeal to familiar derived rules) as
( ac - bd) 2 + ( ad + bc) 2 .
But that, we can see, is just what was wanted, a sum of two integer squares. We have the desired result.
39By formulating the content of the concept with which we began in the formula language of algebra, we were able to reason in the language, by putting equals for equals, to obtain eventually the result that was wanted. That reasoning was, or at least could have been made to be, fully rigorous, every step licensed by a basic or derived rule in the system, but it was also fully contentful. In proving the theorem that the product of two sums of integer squares is also a sum of integer squares (that is, that being a product of two sums of integer squares entails being a sum of integer squares, and vice versa) in elementary algebra one does not abstract from content; instead one expresses content in a mathematically tractable way, in a way enabling reasoning in the system of signs. Of course the beginning student will operate with the language in a fairly mechanical way, much as the beginning chess player operates with chess pieces in the course of a game. It takes time to become literate in the system, to learn to see the meanings in the signs, the contents they express, and this is not surprising. The symbolic language of elementary algebra is quite unlike natural language. It is a specially designed system operating on its own distinctive principles, and it takes practice, and some skill, to learn to use it to its full potential—just as it takes practice, and skill, to become a master chess player, to learn to see the opportunities and hazards in particular configurations of chess pieces.
40There is a further lesson in this example as well. As Avigad (from whom I borrow the example) notes, "the proof uses only the commutativity and associativity of addition and multiplication, the distributivity of multiplication over addition and subtraction, and the fact that subtraction is an inverse to addition; hence it shows that the theorem is true much more generally in any commutative ring" [Avigad 2006, 115]. This is just what I have called the Hilbertian insight again. This little chain of reasoning is valid, and so we know that it is an instance of a rule that can be applied also in other cases provided that the requisite properties hold in those cases. This chain of reasoning does not show that we are, in this case, not in fact reasoning about products of sums and sums of squares, any more than the fact that the rule governing the inference about Felix applies also in other cases shows that in the given case we are not reasoning about Felix. What it shows is that the reasoning can also be applied in other cases as well.
- 16 This is just what we find in [Suppes 1957, Chapter 8].
- 17 Compare Frege's remark, in the introduction to The Foundations of Arithmetic, that "often it is onl (...)
- 18 Tappenden, quotes Michael Spivak, [Spivak 1965, 104]: "Stokes' theorem shares three important attri (...)
41Although in our example the symbolism of elementary algebra enables the display of reasoning from some starting point to the desired conclusion, we have seen that mathematicians in their practice often do not provide such a proof or chain of reasoning but only describe one. In this regard mathematician's proofs are very different from what an account such as Suppes' would lead one to expect. And there is another respect as well in which mathematicians' actual practice diverges from the standard view, and diverges in a way that seems centrally tied to the issue of mathematical understanding. According to the standard view, theorems are proven on the basis of axioms, not on the basis of definitions; although definitions are sometimes discussed in logic, they play no role in reasoning as it is understood by the mathematical logician. Definitions are taken merely to provide abbreviations. As Avigad puts it, "in standard logic textbooks... definitions are usually treated outside the deductive framework; in other words, one views definienda as meta-theoretic names for the formulas they stand for, with the understanding that in the real' formal proof it is actually the definientia that appear" [Avigad 2006, 130].16 What this cannot explain, however, is why it is that, as Tappenden has argued, "mathematicians often set finding the 'right'/'proper'/'correct'/'natural' definition as a research objective, and success—finding the 'proper' definition—can be counted as a significant advance in knowledge" [Tappenden 2008, 256].17 A good definition is often critical to the discovery of an interesting and revealing proof of some theorem; indeed, the right definition can render a result wholly trivial, that is, utterly transparent.18 And when a definition has made a result trivial in this way, mathematicians will tell you that we have fully understood the phenomenon in question. This is very hard to understand if a definition is merely an abbreviation. But again if we consider a case from early modern algebra, we can begin to formulate a more satisfactory alternative.
42In our first example we began with a mathematical idea expressed in English and formulated the content of that idea in the language of elementary algebra. We had in that case no simple mathematical sign for the idea the content of which is given by the complex sign '(a2 + b2)(c2 + d2)'. The fundamental importance of definitions in mathematics is thus not even hinted at by such an example. A different example will do better. Though it does not involve any explicit appeal to definitions (which would involve us in more difficulties than can be adequately addressed here), our second example does constitutively involve identities of the form a = b, where the sign on the left is a simple sign in the language and the sign on the right is a complex sign comprising a whole collection of simple signs. As this example makes clear, the identity is not functioning merely as an abbreviation.
43We begin with the exponential function ex, where e is understood to be some particular number (that is, it is a name for a number as π is): e is the number such that ex is its own derivative. (It can be shown that such a number must exist.) Given that ex is its own derivative, it follows that:
ex = 1 + x + x2/2! + x3/3! + x4/4! + ... + xn/n! + ...
44And we know that this is true because if we take the derivative of the infinite series on the right we will end up with just the same series again: the derivative of the first term is zero, of the second is the first, of the third is the second, and so on. What we have in this identity is, then, on the left, a simple sign for a particular function, and on the right, a very richly articulated collection of signs, one that clearly displays a certain pattern—which is why we need not worry about the fact that we cannot actually write out the whole infinite sequence. Enough of it is given that we know how it will go, and so could extend it arbitrarily far. This identity is furthermore true so we know that one and the same function is designated both by the simple expression on the left and by the complex expression on the right. The two signs do not, however, express the same Fregean sense, as is evident from the fact that we had to argue that the identity was true. But we can also just see that the senses of the two expressions are different insofar as the one expression, 'ex', has no internal arithmetical articulation while the other, the infinite series, has a great deal. Precisely because the expression on the right is complex, one can apply the rules of algebra to the content that is there exhibited in a way that is simply impossible in the case of the simple sign appearing on the left.
45It can also be shown that, under suitable assumptions, the sine and cosine functions can be expressed as power series, namely, these:
sin(x) = x - x3/3! + x5/5! - x7/7! + ...
cos(x) = 1 - x2/2! + x4/4! - x6/6! + ...
And now we are in a position to notice something interesting, namely, that all the terms that appear in the power series expansion of the function ex occur in one or other of the power series for the sine and cosine functions. Only the signs are different. Let us then everywhere replace x in
ex = 1 + x + x2/2! + x3/3! + x4/4! + ... + xn/n! + ...
with ix, where i is by definition such that i2 = -1, to give
eix = 1 + ix + (ix)2/2! + (ix)3/3! + (ix)4/4! + (ix)5/5! + ...
Now we do some standard algebraic manipulations according to the rules to get
eix = 1 + ix - x2/2! - ix3/3! + x4/4! + ix5/5! - x6/6! - ...
And rearranging things a bit, by collecting together the terms that contain i, gives this:
eix = (1 - x2/2! + x4/4! - x6/6! + ... ) + i(x - x3/3! + x5/5! - ... ).
And now we can see that the first series is just that we identified with the cosine function and the second that identified with the sine function. Putting equals for equals thus gives us Euler's famous theorem, eix = cos(x) + isin(x), relating the exponential function and the two trigonometric functions.
46As this example illustrates, mathematical identities involving both simple signs and arithmetically complex signs can play a crucial role in a demonstration. Without the simple signs 'ex', 'sin(x)', and 'cos(x)' we would not be able to recognize our result as a result involving the exponential function and the two trigonometric functions; without the power series with which these three functions were identified, we would be unable to reason our way to the desired result. The example thus illustrates the way in which finding a fruitful articulation of some mathematical notion, one that will enable the proof of some result, can constitutes a real mathematical advance. Of course the simple signs are eliminable in the demonstration in the sense that replacing all instances of them in the course of reasoning with the relevant complex signs will not affect the validity of the reasoning. But equally obviously doing that destroys the interest of the demonstration insofar as it is no longer possible to see the demonstration as a demonstration involving the exponential and trigonometric functions. What one would end up with in that case would be a trivial identity, one with the same power series on both sides of the identity sign. Euler's theorem is mathematically significant because it reveals a connection between two apparently independent mathematical domains, that of exponential functions and that of trigonometric functions. But we can see this only if we have the identities of the exponential function and of the trigonometric functions with which we began, both the complex signs, the power series, and the simple signs 'ex', 'sin(x)', and 'cos(x)'.
47By displaying the contents of mathematical notions of antecedent interest in new and mathematically tractable ways, identities enable demonstrations involving those notions, and they can do because, as we have just seen, in the identities those contents are displayed in complex signs in ways that enable reasoning. In these identities, both the simple sign and the complex sign designate or mean one and the same thing; they have the same Bedeutung.
48But, again, they do not express the same sense; they have quite different roles to play in the process of reasoning. Different things follow from the simple and the complex signs precisely because the one is a simple sign and the other is a complex sign with a lot of internal articulation that can be utilized in the proof. And though I will not try to show it here, just the same point can be applied also to definitions in actual mathematical practice. Definitions in mathematics are not mere abbreviations. They provide an articulation of the content of some mathematical notion that is also named in the definiendum, content that can be critical to the chain of reasoning required by the proof.
49I have suggested that we think of axioms, for instance, those of elementary algebra, as ascriptions of basic properties to arithmetical operations such as addition and multiplication. Theorems derived from those axioms ascribe further properties to those operations, and both those axioms and the theorems derived from them can then be treated as basic and derived rules governing valid inferences. We have looked at two sorts of cases, one that did not involve any identities of simple and complex signs (our little demonstration of the theorem that if two numbers are both sums of integer squares then their product is also a sum of integer squares) and another in which such identities have an essential role to play, namely, in the demonstration of Euler's theorem. In both sorts of cases the reasoning is, in principle, fully rigorous; every step in the reasoning is justified by some antecedently specified (or specifiable) rule. But the reasoning is also fully contentful. The formula language of arithmetic and algebra enables the expression of a content in a way that is mathematically tractable, that is, in a way enabling one to reason (on the basis of content) in the system of signs. And because it does, we can begin at least to understand, if only for this case, how it is that a proof can advance our mathematical understanding. Because the dilemma with which we began—according to which a proof cannot be both formal, that is, fully rigorous, and also contentful (hence relevant to mathematical understanding)—does not arise for this case, we can see how a fully rigorous chain of reasoning can be fully compatible with reasoning on the basis of mathematical ideas. Our examples show that it is possible that by proving something a mathematician might gain insight and understanding.
- 19 I owe the phrase "Denken in Begriffen" to Detlef Laugwitz in [Laugwitz 1995].
50Over the course of the nineteenth century the practice of constructive algebraic problem solving, that we see, for instance, in Euler's work, began to give way, in the work of Riemann, Dedekind, and others, to a new sort of mathematical practice, the practice of reasoning deductively from defined concepts, Denken in Begriffen, thinking in concepts.19 Because there was no mathematical language, no system of written signs within which to do this work, proofs had to be reported (as they are still today) in natural language together with whatever help could be provided by the formula language of arithmetic and algebra. Taking our cue from that formula language, it is, however, possible to say what such a system of signs would have to do: it would have to formulate the inferentially articulated contents of the concepts of mathematical interest in a way that enables mathematical reasoning. Our logical languages were not designed to do this. Although one can formulate basic and derived laws of logic in a logical language such as that Suppes introduces in his little logic textbook, and can reason rigorously in the system, one cannot exhibit the contents of concepts in such a language. The language was not designed for that expressive purpose, and nor even is it obvious how this might be done, what sort of language might be needed instead.
- 20 In [Macbeth 2005], I outline the reading of Frege's notation that I would argue is needed here. See (...)
51It seems in a way obvious that an expression of algebra such as a2 + b2 ' formulates the content of the mathematical idea of a sum of two integer squares, that it displays what it is to be such a sum. But as obvious and natural as this is to us, it is far from clear how the language is functioning to enable such a display. And because this is not clear such an expression does not immediately suggest to us what it would take to display the contents of concepts in a way that would enable not now algebraic computations but instead deductive reasoning, that is, the sort of reasoning mathematicians began to employ over the course of the nineteenth century. But we do know at least this much. Because the reasoning involved in this case is deductive rather than algebraic, the contents of our concepts would need to use signs for logical relations in much the way, in elementary algebra, we use signs for arithmetical operations. As in algebra we introduce a few primitive signs for the basic arithmetical operations, so we would need to introduce a few primitive signs for the basic logical relations, say, the conditional, negation, and identity, as well as a sign usable in the expression of generality of content. We would then need to formulate axioms, corresponding to the axioms of algebra, that would set out the basic properties of those primitive logical relations, and to derive some theorems from those axioms. As in algebra, the axioms and derived theorems would then function as rules governing inferences in the system. Definitions of concepts of antecedent mathematical interest could then be formulated in the system and those definitions could provide the starting point for proofs much as identities formed the starting point for our little demonstration of Euler's theorem. That is what we would need … and that, I would argue (though of course I cannot do so here), is what is provided for us already in Frege's 1879 Begriffsschrift, his concept-script. Frege explicitly and self-consciously designed his strange two-dimensional notation to express mathematical content in a way that would enable rigorous reasoning on the basis of that content. And in Part III of his 1879 logic, he proves a theorem on the basis of explicit definitions that aims to illustrate precisely how a strictly deductive proof in his language can be ampliative, that is, constitute real extension of our knowledge. If Frege is right, his language is just what we need to display rather than merely to describe both the contents of mathematical concepts and the chains of reasoning that take us from definitions of concepts to theorems revealing logical relations among those defined concepts. Of course, we will not be able even to begin to understand how this could be so, so long as we continue to read his notation as a mere variant of our own.20
52Proofs in mathematics can take many forms, and can contribute to mathematical understanding in a very wide variety of ways. What I have said here only touches on one point, but it is a point that is, I think, central. In order to understand the role of proving theorems in achieving mathematical understanding, we need better to understand what a mathematical proof is, and in particular, the role that specially devised systems of written marks have historically played in the mathematical practice of proof, how they have served to formulate content in ways that facilitate rigorous mathematical reasoning. Standard mathematical logic is not such a system of signs; nor, again, was it designed to be. Rather than formulating content as it matters to inference in mathematical practice (as Frege's concept-script was designed to do, and I would argue succeeds in doing) standard notations of logic introduce abbreviations, special signs to take the place of words, to enable the perspicuous display of the logical forms of sentences of natural language. Little wonder, then, that a mathematical proof fully formalized in standard notation is unintelligible.
- 21 This is often the case, but not always. The ancient proof that there is no largest prime is reporte (...)
- 22 An earlier version of this paper was presented at the conference, The Notion of Form in 19th and Ea (...)
53Lacking any adequate system of signs within which to reason deductively from the contents of defined concepts, mathematicians in their practice today—at least in cases in which the reasoning is deductive from concepts rather than algebraic—can only report the course of their reasoning; they describe how it goes rather than showing how it goes in a specially devised system of written marks. And as anyone who has worked on results in algebra that were discovered before the development of an adequate symbolism for (elementary) algebra knows, it is often much harder to understand a proof that is only described than it is to follow one in which the reasoning is displayed.21 But there is another problem as well: where the reasoning is not displayed in a system of written marks but only reported it is much harder to come to understand how the reasoning works as reasoning. We will not understand how a mathematical proof can yield mathematical understanding until we understand much better than we currently do how it is that one reasons on the basis of content in mathematics. And to understand that we must concern ourselves with how content is formulated in specially devised systems of signs in actual mathematical practice—in Euclidean diagrams, in algebraic equations, and (I would argue) in Frege's Begriffsschrift formulae.22