An Analysis of the Notion of Rigour in Proofs
Michèle Indira Friend, Andrea Pedeferri · 2011
We are told that there are standards of rigour in proof, and we are told that the standards have increased over the centuries. This is fairly clear. But rigour has also changed its nature. In this paper we assess where these changes leave us today. 1 To motivate making the new assessment, we give two illustrations of changes in our conception of rigour. One, concerns the shift from geometry to arithmetic as setting the standard for rigour. The other, concerns the notion of effective proof or computations. To make the assessment, we look at one motivation for increasing the rigour of a mathematical argument: explicitness and honesty. We then present a standard of rigour by means of a characterisation developed with reference to what we call ‘an account-proof’. We evaluate the standard with reference to the motivation. With the analysis we discover that, regardless of the motivations for rigour, the standard is almost never met, and that the motivations are not all satisfied. It follows that, in some sense, the motivations have misfired. The misfiring suggests to 1 In this paper, we make a negative point about the state of play today. The reckoning prepares the ground for a future paper where we make a more positive point about how we should develop the conception of rigour today. COGNOME E NOME PRIMO AUTORE, COGNOME E NOME SECONDO AUTORE 166 us that we re-assess our notion of rigour. We think of rigour as a relative term. Moreover, the standard for rigour depends on philosophical underpinnings. The strength of the argument of this paper rests on the plausibility of our selection of motivations and on the plausibility of our standard. 1. Meeting the Ideal Standards of Rigour 2 Rigour in proof can be variously motivated, but here, we only consider the motivation of explicitness and honesty. The reason we want a proof to be rigorous is to be quite honest and explicit about our best reasons for accepting the conclusion. ‘Explicitness and honesty’ are not meant in the sense of private conviction or emotions but in their scientific sense. They invite possible objections to given proofs. When explicitness is our motivation, we have in mind the possibility of doubt or dispute. An explicit proof can be easily checked. Scrutiny is important. In mathematical proofs, it is not enough (except in some applications) that an inference is probably O.K., it has to be definitely correct. The notion of correctness used here is not an absolute notion, transcending all of mathematics. Instead, we follow Cellucci in thinking of mathematical proofs as, what he calls “analytic proofs” (Cellucci 2008). In such a proof, when we make it explicit, we expose several features to scrutiny. Internal to the proof, we have the reasoning. External to the proof, there is the conjectural aspect of the theorem, which is purportedly proved. This can be thought of as an invitation to explore the limitations of the results: the limitations of the theorem, the independent credibility of the theorem and the justifications for the theorem. Exploring the limitations and credibility of a theorem, or proof, is done by looking at the theorem from outside: from a metaperspective. We look at the axioms, rules of inference and the context, or intended interpretations. In full (ideal) rigour we would prove in a meta-theory that a proof is sound and valid. If we know the meta-theory within which the proof is acceptable, we know a lot about the scope of the proved theorem. It 2 This paper was presented at both the ASL Logic Colloquium, Paris, 25 – 31 July 2010 and at SiLFS in Bergamo 15 – 17 December 2010. We should like to thank the audiences at both for their questions and comments. The paper was inspired by discussions between Michele Friend and Andrea Pedeferri. A longer version is being prepared, in which we investigate seven motivations for rigour, not just one. However, we think that this one is the most interesting. TITOLO DEL CONTRIBUTO 167 will be true along with every theorem of all the theories verifiable by that (class of) meta-theory(ies). Alas, the ideal is seldom reached. We judge correctness, or evaluate a proof, by reference to background knowledge. The background knowledge might include a number of theories, some quite abstruse (which is why only some people are qualified to verify some proofs). For example, some proofs require the existence of some remote large cardinals, embedded in a foundational theory. This knowledge is not only enjoyed by the few, it is also and odd type of verification since, paraphrasing (Thurston 1994, p. 171), it is more dubious than the theorem being checked. Worse, the relation between a proof and doubting, questioning or checking a proof is not tight or complete in practice, since we might not know what the maximal meta-theory is, so what the maximal scope of the theorem is. Also, we might not know what the minimal meta-theory is, so the minimum needed to justify a theorem. Worse still, we might not have a particular meta-theory in mind at all, and might just help ourselves to “whatever it takes” or “whatever seems appropriate” to verify a proof. So the “theory” in “meta-theory” might not be an explicit theory at all, but more “background knowledge”, and a sense of general context. We presume that we can make it more explicit if necessary, i.e., if further doubt arises. This presumption is not guaranteed to be justified. Let us begin with the ideal, of matching explicitness with rigour. We’ll later address our shortcomings in our practice of mathematics. 2. A Characterization of Rigour We are heading towards the following characterisation: A proof is rigorous iff it is an account-proof. “Account-proof” is a technical term. The term is new but the concept is not. It is what the constructivists would call a demonstration, or deduction. But since “deduction” is used a little more loosely now, we shall introduce a new term to rekindle an old idea. Definition: An “account-proof” is a proof that proceeds from axioms or premises, and in which every line of proof is accounted for by reference to a rule of deduction or by appeal to an axiom, premise or definition. COGNOME E NOME PRIMO AUTORE, COGNOME E NOME SECONDO AUTORE 168 The rules, axioms, premises and definitions have to meet certain criteria. The premises and definitions are easy, so we begin with those. Definitions, in an account-proof, are simply short-hand expressions. So nothing new is introduced when we appeal to a definition. Premises have to be truth-apt wffs, (or justifiable wffs). The criteria are the same for axioms and rules since an axiom can be expressed as a rule, and a rule can be expressed as an axiom. 3 Henceforth, we shall simply use the term “axiom” as standing for “axiom and/ or its equivalent rule”. Axioms are immediate judgments: formulas that are self-justifying. Self-justification is justification in terms of meaning. Slogan: A self-justifying axiom is an axiom that is true in virtue of the meaning of the symbols used in the wff. Symbols can be given a meaning in a separate semantics, as we would in model theory, or in terms of manipulation rules, as we would in proof theory. Self-justifying axioms are usually thought to be fixed. However, meaning is not a fixed entity. It changes and evolves. It is dynamic, and is born of a dialectic between formal representation and informal understanding. We give the following account of meaning: we start with a concept, which is not completely precise. We might find that we are dissatisfied with the imprecision, or that we are encountering conflicts or difficulties. As a bid for clarity we could try the strategy of giving the concept a symbol to give it some sort of formal representation. We give axioms, written in the formal language, that are supposed to capture the essential aspects of the concept. What the formal representation does is to give a very rigid, 4 precise and abstract (but ultimately revisable) “formal meaning” to the concept. We then become familiar with the formal meaning. We can then re-check it. We ask if the formal meaning corresponds to the previous informal meaning. The answer might not even be a “yes” or “no” answer. We might discover that the original idea contained subtle nuances, of which we were not aware. We could then make two formal representations. Or, it might be that we have discovered that the informal concept was hope3 The difference is that rules have the connotation of an action, whereas axioms have the connotation of a fixed eternal truth. Since we can inter-translate axioms and rules, the connotations can be taken quite separately, and we can ignore them here. 4 We elaborate on the rigidity in a follow-up paper from this one. TITOLO DEL CONTRIBUTO 169 less because it leads to other problems. Or we might say that our informal understanding has been changed to take on the formal meaning. Since each of these is a possibility, formal representation is thought of as adding to the meaning of an expression. Here “the meaning” (informal and formal) is located somewhere beyond both the initial concept and the formal version of the concept. Moreover the concept changes with the dynamics of formal representation. In light of this account of meaning, we can elaborate on our slogan. An axiom being “self-justified” is revisable! An axiom is self-justified iff after an honest search, we have found no further justification, and it makes better sense of the concepts in the axiom than the alternatives we have looked at. We made all of these qualifications concerning criteria for being an axiom, a rule, a premise or a definition in order to understand the definition of an account-proof, which we repeat is: a proof that proceeds from axioms or premises, and in which every line of proof is accounted for by reference to a rule of deduction or by appeal to an axiom, premise or definition. We did this, in order to characterise rigour. A proof is rigorous iff it is an account-proof.