Navigation – Plan du site

Mathematical Rigor, Proof Gap and the Validity of Mathematical Inference

Yacin Hamami
p. 7-26

Résumés

Mathématiciens et philosophes définissent communément la rigueur mathématique de la manière suivante : une preuve mathématique est rigoureuse dès lors qu'elle ne présente aucun « trou » dans le raisonnement mathématique qui la compose. Toute approche philosophique de la rigueur mathématique formulée suivant cette conception se doit de définir la notion de « trou ». Cependant, une telle notion ne peut être pensée que relativement à une conception du raisonnement mathématique valide, i.e., de la validité de l'inférenee mathématique. Un « trou » dans une preuve mathématique peut ainsi être conçu comme un échec dans la production d'une inférence mathématique valide. L'objectif de cet article est d'évaluer deux conceptions de la validité de l'inférence mathématique par rapport à leur capacité à fournir une explication plausible des notions intuitives de « trou » présentes dans la pratique mathématique. La première conception est issue des standards contemporains de la rigueur mathématique : une inférence mathématique est valide si, et seulement si, sa conclusion peut être dérivée formellement à partir de ses prémisses. Nous montrerons que cette conception ne peut fournir une explication plausible des notions intuitives de « trou » dans les preuves mathématiques. La seconde conception est issue d'une nouvelle approche de la validité de l'inférence proposée par Prawitz : une inférence est valide si, et seulement si, elle consiste en une opération produisant une justification pour sa conclusion à partir de justifications pour ses prémisses. Nous adapterons tout d'abord cette conception à l'inférence mathématique et nous montrerons alors qu'elle est en mesure d'accommoder différentes notions intuitives de « trou » à travers différents types d'échecs dans la production d'inférences mathématiques valides. Nous conclurons en soulignant l'intérêt de cette conception pour la philosophie de la pratique mathématique, et nous relèverons un certain nombre de défis confrontant le développement d'une telle approche des notions de rigueur mathématique, de « trou » et de validité de l'inférence mathématique.

Haut de page

Texte intégral

The author would like to thank Jean Paul van Bendegem and John Mumma for helpful comments and stimulating discussions relative to this paper. The author is a doctoral fellow of the Research Foundation Flanders (FWO).

1 Introduction

  • 1 See for instance Kitcher: "central to the idea of rigorous reasoning is that it should contain no g (...)
  • 2 We do not claim that this formulation exhausts the notion of mathematical rigor, nor are we trying (...)

1Mathematical rigor is commonly formulated by mathematicians and philoso­phers using the notion of proof gap1: a mathematical proof is rigorous when there is no gap in the mathematical reasoning of the proof.2 Any philosophi­cal approach to mathematical rigor along this line requires then an account of what a proof gap is. However, the notion of proof gap makes sense only rela­tively to a given conception of valid mathematical reasoning. A natural way to state the connection is the following: a proof gap occurs in a mathemati­cal proof whenever there is a failure in valid mathematical reasoning. If one considers valid mathematical reasoning to consist in chains of valid mathemat­ical inferences, the connection becomes: a proof gap occurs in a mathematical proof whenever there is a failure in drawing a valid mathematical inference. In order to characterize the notion of proof gap in this way, one shall then
(i) provide an account of what constitutes a valid mathematical inference and
(ii) spell out how one can fail to draw a valid mathematical inference in the specified sense.

2The aim of this paper is to explore two possible views of the validity of mathematical inference with respect to their capacity to yield a plausible account of the intuitive notion(s) of proof gap from mathematical practice. The first view is the one provided by the contemporary standards of mathematical rigor based on the notion of formal derivation: a mathematical inference is valid if and only if its conclusion can be formally derived from its premises. The second view is based on a new account of the validity of inference developed by Prawitz [Prawitz 2009, 2012a, b]: a mathematical inference is valid if and only if it consists in an operation that provides a ground for its conclusion given (previously obtained) grounds for its premises. To evaluate these two views, we will proceed as follows: (i) we will state in precise terms the two conceptions of the validity of mathematical inference they propose, (ii) we will spell out the notions of proof gap they give rise to by investigating how one can fail to draw a valid mathematical inference in the specified sense, (iii) we will evaluate the capacity of the resulting accounts to capture the intuitive notion(s) of proof gap from mathematical practice.

3We will place our investigation within the framework of the philosophy of mathematical practice ([Mancosu 2008], [van Kerkhove & van Bendegem 2010]). This means that we will not only consider mathematical proofs and mathematical reasoning from contemporary mathematical practice, but also from different practices at various times in the history of mathematics. Consequently, by a mathematical inference, we will mean an inferential or deductive step of a mathematical proof in mathematical practice (past or present). Such proof steps are often signaled in mathematical proofs by ex­pression such as "hence", "therefore", "it follows that", etc. Then, by a valid mathematical inference, we will mean a mathematical inference that is correct or sound by the standards of mathematical proof in mathematical practice. Finally, by the intuitive notion(s) of proof gap, we will refer to the notion(s) of proof gap that is (are) present in mathematical practice. Providing a philo­sophical account of these three notions appears as a central task for the phi­losophy of mathematical practice.

4The paper is organized as follows. In section 2, we formulate three derivation-based accounts of the validity of mathematical inference based on three possible interpretations of the relation between the notions of rigorous mathematical proof and formal derivation. We then spell out the resulting derivation-based accounts of proof gap, and we provide arguments for their rejections as adequately capturing the intuitive notion(s) of proof gap from mathematical practice. In section 3, we present Prawitz's recent account of the validity of inference based on the notions of operation and ground. In sec­tion 4, we adapt Prawitz's account to mathematical inference, resulting in a ground-based account of the validity of mathematical inference, by specifying the notions of operation and ground in the context of mathematical proofs in mathematical practice, where the notion of mathematical practice will be provided by Kitcher's framework [Kitcher 1981, 1984]. Sections 5 and 6 are concerned with evaluating the capacity of the resulting ground-based account of proof gap to capture the intuitive notion(s) of proof gap from mathematical practice. Section 5 focuses on intra-praxis gaps—proof gaps that occur within a given mathematical practice—and shows that the ground-based account can capture the three kinds of proof gaps constituting the taxonomy proposed in [Fallis 2003] as particular types of failure that will be identified. Section 6 fo­cuses on inter-praxis gaps—proof gaps that occur from a cross-perspective on different mathematical practices—and shows how they can as well be accom­modated within the ground-based account. Section 7 concludes this paper by wrapping up the main results of our evaluation of the two views of the validity of mathematical inference through the accounts of proof gap they give rise to, and by raising several challenges facing a full development of a ground-based account of the notions of mathematical rigor, proof gap and the validity of mathematical inference.

2 Derivation-based accounts of the validity of mathematical inference

5According to [Detlefsen 2009], the contemporary prevailing view of what a rigorous mathematical proof is can be stated as follows:

Rigorous proof [...] is reasoning all of whose inferences track purely logical relations between concepts. In the late nineteenth and early twentieth centuries, syntactical criteria for such relations were developed and these have become the basis for the currently prevailing view of formalization. [Detlefsen 2009, 17]

6What Detlefsen refers to in this quote by 'syntactical criteria' corresponds to the modern notion of formal derivation from proof theory. The prevailing view of mathematical rigor leaves then room for different interpretations of the relation between the notions of rigorous mathematical proof and formal derivation. In this section, we will consider three possible interpretations: (i) a mathematical proof is rigorous if it is a formal derivation, (ii) a mathematical proof is rigorous if it can be turned into a formal derivation, (iii) a mathe­matical proof is rigorous if it can routinely be turned into a formal derivation. These three interpretations lead to three different accounts of the validity of mathematical inference, and thereby to three different notions of proof gap. We will now evaluate them in turn with respect to their capacity to capture the intuitive notion(s) of proof gap from mathematical practice.

  • 3 This observation has been used to argue that "rigor and formalization are independent concerns" [De (...)

7The first interpretation yields the following account of the validity of math­ematical inference: a mathematical inference is valid if and only if its conclu­sion has been formally derived from its premises. Prom this definition, it is straightforward to state what it means to fail in drawing a mathematical infer­ence: it simply means to fail in providing a formal derivation of the conclusion of the inference from its premises. This yields the following notion of proof gap: a proof yap occurs in a mathematical proof whenever there is a math­ematical inference in the proof for which no explicit formal derivation of the conclusion from the premises has been provided. This account of proof gap is over-generative, in the sense that it recognizes proof gaps in mathematical proofs that are considered as gapless in mathematical practice. The easiest way to see this is to notice that most mathematical proofs that are considered in mathematical practice are not presented under the form of formal derivations.3 In particular, these mathematical proofs contain mathematical inferences for which no formal derivation of the conclusion from the premises has been pro­vided. If one adopts the notion of proof gap just stated, one is then forced to recognize proof gaps in most ordinary mathematical proofs. This notion is therefore over-generative and does not correspond to an intuitive notion of proof gap present in mathematical practice.

8The second interpretation yields the following account of the validity of mathematical inference: a mathematical inference is valid if and only if its conclusion can be formally derived from its premises. This leads to the follow­ing notion of proof gap: a proof gap occurs in a mathematical proof whenever there is a mathematical inference in the proof for which no formal deriva­tion of the conclusion from the premises can be provided. This account of proof gap is under-generative, in the sense that it does not recognize proof gaps in mathematical proofs when there are ones according to the standards of mathematical practice. To see this, consider any theorem for which a for­mal proof has been provided in a modern proof assistant (HOL Light, Coq, Isabelle, etc.), for instance the prime number theorem for which a formal proof has been provided in Isabelle [Avigad, Donnelly et al. 2007]. In this particular case, the mathematical inference consisting of the prime number theorem as conclusion, and of the axioms of higher-order logic, along with an axiom asserting the existence of an infinite set, as premises, is such that its conclusion can be formally derived from its premises. This mathematical inference is then valid according to the account just stated. Consequently, the mathematical proof consisting of this particular mathematical inference alone should be considered as gapless, which is obviously at odds with mathemati­cal practice. We shall then conclude that this notion is under-generative and therefore does not correspond to an intuitive notion of proof gap present in mathematical practice.

  • 4 This view is expressed for instance by Mac Lane: "In practice, a proof is a sketch, in sufficient d (...)
  • 5 This point has been acknowledged by Robinson, one of the main figures in automated theorem proving, (...)

9The third interpretation yields the following account of the validity of mathematical inference: a mathematical inference is valid if and only if its conclusion can routinely be formally derived from its premises. This leads to the following notion of proof gap: a proof gap occurs in a mathematical proof whenever there is a mathematical inference in the proof for which no formal derivation of the conclusion from the premises can be routinely provided. This interpretation is probably the most faithful to the defenders of the prevailing view of mathematical rigor who argue that, even though rigorous mathemati­cal proofs are not usually presented as formal derivations, they can routinely be turned into formal derivations.4 The main issue with this account is to provide a precise meaning of what it means for a mathematical inference to be routinely formalizable, i.e., to be turned routinely into a formal derivation of the conclusion from the premises. One way to address this issue is to look at the field of formal verification, where the main goal is to provide actual formal derivations of mathematical theorems that can be checked in a purely mechan­ical way by a proof assistant. What the research activity in this field seems to reveal is that it is almost never a routine affair to provide a formal derivation from an existing ordinary mathematical proof.5 In particular, there does not seem to be any direct meaningful sense that can be attributed to the idea of a routine translation of a mathematical inference into a formal derivation. Consequently, the notion of proof gap provided by the third interpretation should not be rejected as inadequate, but rather as underdetermined.

  • 6 For some historical examples of changes in mathematical rigor, see [Kitcher 1981], [Pierpont 1928].
  • 7 We will come back to this point at the end of section 6.

10The three derivation-based accounts of the validity of mathematical infer­ence proposed in this section do not yield an account of proof gap that would capture adequately the intuitive notion(s) of proof gap from mathematical practice. Yet, there is still a more general reason to doubt any derivation-based account of the validity of mathematical inference. The reason is that, from the perspective of the philosophy of mathematical practice, a philosophi­cal account of the validity of mathematical inference and of the notion of proof gap should not only be adapted for contemporary mathematical practice, but also for other mathematical practices from the history of mathematics. In par­ticular, such an account should be able to accommodate changes in standards of mathematical rigor over different mathematical practices, as it occurred many times in the history of mathematics.6 To this purpose, any derivation-based account would appear far too rigid, in the sense that it would provide an absolute or fixed point of reference for determining what constitutes a valid mathematical inference and a proof gap, and therefore shall fail to account for different standards.7 The second view of the validity of mathematical infer­ence that we will discuss in the next sections promises to offer more flexibility in this respect.

3 Prawitz on the validity of deductive inference

  • 8 In this section, when we will use the term inference, we will always refer to deductive inference.

11In a series of papers [Prawitz 2009, 2012a,b], Prawitz has undertaken the task to develop a new conceptualization of the notion of valid deductive inference.8 The main motivation for this project comes from the requirement that, ac­cording to Prawitz, a philosophical account of the validity of inference should be able to explain how one can acquire justifications or grounds by drawing valid inferences. More precisely, such an account should lead as a concep­tual truth that by drawing a valid inference, one can acquire a ground for the conclusion given grounds for the premises that one is already in posses­sion of. According to Prawitz, neither the notion of logical consequence from model theory nor the notion of formal derivation from proof theory have been able to address this requirement [Prawitz 2012a, 888]. Prawitz's solution is to build the grounding requirement directly into the conception of the validity of inference. More specifically, Prawitz proposes an account of the validity of inference where inferences are conceived as operations on grounds:

To get a fresh approach to the concept of valid inference we should reconsider the concept of inference. As already noted, a typical way of announcing an inference is to make an assertion and state at the same time a ground for the assertion, saying for instance "B, because A" or "A, hence B". [...]
Although the conclusion and the premises may be all that we make explicit, there is also some kind of operation involved thanks to which we see that the conclusion is true given that the premises are. Sometimes we vaguely refer to such an operation [...], but es­sentially it is left implicit. My suggestion is that in analysing the validity of inferences, we should make these operations explicit, and regard an inference as an act by which we acquire a justifi­cation or ground for the conclusion by somehow operating on the already available grounds for the premises. [Prawitz 2012b, 18]

The validity of inference is then defined as follows:

An individual inference is valid if and only if the given grounds for the premises are grounds for them and the result of applying the given operation to these grounds is in fact a ground for the conclusion. [Prawitz 2012b, 19]

12There are thus two central notions to Prawitz's account of the validity of inference: operation and ground. We shall now see how they are defined, starting with the notion of ground.

13The term ground is used by Prawitz as a synonym for justification: to have a ground for a statement A means to be justified in holding A true [Prawitz 2012a, 890]. The main issue is then to determine how the notions of ground and statement are related, i.e., to specify what constitutes a ground for a statement. Prawitz's solution is to appeal to a specific theory of meaning:

The line that I shall take is [...] roughly that the meaning of a sentence is determined by what counts as a ground for the judge­ment expressed by the sentence. Or expressed less linguistically: it is constitutive for a proposition what can serve as a ground for judging the proposition to be true. Prom this point of view I shall specify for each compound form of proposition expressible in first order languages what constitutes a ground for an affirmation of a proposition of that form. [Prawitz 2009, 19H92]

14For instance, in the case of conjunction, Prawitz proposes the following spec­ification: α is a ground for the conjunction p q if and only if α = G(β, γ) for some β and γ such that β is a ground for p and γ is a ground for q. Such specifications rely on grounding operations, such as the conjunction grounding operation G, which specify how grounds for a certain type of statement shall be formed. These grounding operations are primitive in Prawitz's account. In the case of the statements expressible in first-order logic, the grounding op­erations closely follow the introduction rules of natural deduction. Notice, however, that this ground-based account of meaning is not restricted for Prawitz to the language of first-order logic, even though explicit descriptions of grounding operations are only provided for first-order statements. Notice also that, according to this theory of meaning, if an agent understands the mean­ing of a statement, she then has the capacity to recognize what constitutes a ground for it.

  • 9 A formal description of this operation has been proposed by Prawitz in [Prawitz 2012a, 897].

15The second key notion in Prawitz's account of the validity of inference is the one of operation on grounds. Prawitz does not provide a general definition of what exactly these operations are, except that they have grounds as input and output. However, Prawitz does provide concrete examples of operations for the logical inferences corresponding to the inference rules of natural deduction for first-order logic, as well as for mathematical induction. In particular, all the grounding operations corresponding to the introduction rules of natural deduction constitute such operations. For instance, the conjunction grounding operation G is an operation that takes as input a ground γ for p and a ground β for q, and outputs a ground α = G(β, γ) for the conjunction p q. Regarding mathematical induction, an informal description of the associated operation has been provided by Prawitz as follows:9

Let us consider the inference form of mathematical induction, in which it is concluded that a sentence A(n) holds for an arbitrary natural number n, having established the induction base that A(0) holds and the induction step that A holds for the successor n' of any natural number n given that A holds for n. The ground for the induction step may be thought of as a chain of operations that results in a ground for A(n') when applied to a ground for A(n). The operation that is involved in this inference form may roughly be described as the operation which, for any given n, takes the given ground for A(') and then successively applies the chain of operations given as ground for the induction step n times. [Prawitz 2012b, 20]

16We can now state what drawing a valid inference consists in for Prawitz: it means applying the given operation to the grounds of the premises and to verify that the result is indeed a ground for the conclusion. Since understanding the meaning of the statements involved in the inference is a necessary precondition for being able to draw a valid inference [Prawitz 2009, 199], the agent does have the capacity to recognize what constitutes a ground for the conclusion and can therefore evaluate whether the result of the operation is indeed a ground for the conclusion. In the example of conjunction, the inference with premises p and q and conclusion pq is trivially valid since, given grounds β for p and γ for q, applying the operation G to p and q results in G(β, γ) which is a ground for p q according to the above specification. In the example of mathematical induction, the inference with premises A(0) and A(n) → A(n+1) and conclusion nA(n) is valid since the application of the above operation for mathematical induction to the grounds for the premises yields a groundfor A(n), and this for any natural number n.

17How according to the ground-based account one can fail in drawing a valid inference? As we shall see in the next sections, there are several possible ways to fail in drawing a valid inference, which will lead in turn to different kinds of proof gaps. However, if we want to be able to evaluate the notions of proof gap resulting from Prawitz's account of the validity of inference, we first need to specify it in the particular case of mathematical inference.

4 A ground-based account of the validity of mathematical inference

  • 10 As also noted by Pagin: "A main point of Prawitz's discussion [...] is that it does not solely appl (...)

18Prawitz's conception of the validity of inference is not only meant as a general account of the validity of deductive inference in formal proof systems such as natural deduction, but also of the validity of what we might call informal deductive inference.10 Since mathematical inferences are par excellence a type of deductive inference which provide conclusive grounds for their conclusions, and that most mathematical inferences in mathematical proofs are informal deductive inferences, mathematical inference fits perfectly within the scope of Prawitz's account. Indeed, Prawitz confirms this application by taking as one of the key illustrative examples of his account the validity of mathematical induction, the archetypal example of a mathematical inference.

19How can we adapt Prawitz's account to the specific context of mathemat­ical inference? As we saw in the previous section, the main task is then to specify the central notions of this account—i.e., the ones of operation and ground—in the context of mathematical proofs in mathematical practice. To this end, it would appear particularly useful to start with a more precise conception of what a mathematical practice is. For this purpose, the most natural choice is to adopt the framework developed by Kitcher in [Kitcher 1981, 1984]. In this framework, a mathematical practice is described as a tuple L, M, Q, R, S where: L is the language of the practice, M the set of meta-mathematical views, Q the set of accepted questions, R the set of accepted reasonings, and S the set of accepted statements. The two components directly relevant to the issue of the validity of mathematical inference are theset of accepted reasonings R and the set of metamathematical views M. We shall now see how Kitcher defines these two components, and how they shouldbe adapted to integrate the notions of operation and ground within the notion of mathematical practice.

20The set of accepted reasonings R is defined by Kitcher as: “the sequences of statements mathematicians advance in support of the statements they assert” [Kitcher 1984, 180]. As we saw in the first quote of the previous section, Prawitz does not identify an inference only by its premises and conclusion, but also by some operation that should be made explicit. Consequently, we shall consider the set of accepted reasonings R as constituted of a set of mathematical inferences, where an inference is identified not only by its premises and conclusion, but also by the operation involved. For instance, inferences cor­responding to mathematical induction should not only be identified by their premises A(0) and A(n) → A(n + 1) and conclusions ∀nA(n), but also by the operation described in the previous section. Mathematical induction is here a perfect example of mathematical inferences members of the set of accepted reasonings in the mathematical practice of contemporary number theory. For other examples we can mention: the diagrammatic inferences in the mathemat­ical practice of elementary Euclidean geometry in Euclid's Elements [Euclid ana], the computer-assisted inferences in the mathematical practice of graph theory, or the use of numerical methods—also known as experiments—in var­ious mathematical practices such as number theory or analysis. Notice that all these examples of mathematical inferences members of the set of accepted reasonings do not necessarily yield valid mathematical inferences. This is an interesting and important aspect of Kitcher's framework, namely that: "the set of accepted reasonings will outrun the set of accepted proofs" [Kitcher 1984, 181]. As examples of types of accepted reasoning that do not constitute proofs, Kitcher mentions reasonings that might be used to warrant beliefs, such as inductive generalizations in number theory, or reasonings that appear unrigorous, such as various methods of reasoning with infinitesimals in the early development of the calculus. According to Kitcher, whether an accepted reasoning in a mathematical practice constitutes a proof and, in our termi­nology, whether a mathematical inference is valid, is determined by the set of metamathematical views.

21The set of metamathematical views M is defined by Kitcher as containing at least the following components: (

i) standards for proof; (ii) the scope of mathematics; (iii) the order of mathematical disciplines; (iv) the relative value of par­ticular types of inquiry. [Kitcher 1984, 189]

22For our purposes, the only relevant component will be the standards of proof. According to Kitcher, these standards can be specified “by describing the kinds of inference which are held to be legitimate, or by indicating paradigms of the type of reasoning which is preferred” [Kitcher 1984, 190]. However, since we want to reach an account of the validity of mathematical inference, we do not want to define the correct inferences simply as elements in the set of meta­mathematical views. Rather, we want the set of metamathematical views to specify what constitutes a ground for a mathematical statement that can be formulated within the considered practice. In other words, we shall substi­tute, in the set of metamathematical views of a given mathematical practice, standards of proof for standards of justification or ground for mathematical statements.

23Thus, our two main modifications of Kitcher's notion of mathematical prac­tice consist in (i) identifying mathematical inferences in the set of accepted reasonings R not only by their premises and conclusions but also by the operations involved, and (ii) replacing in the set of metamathematical views M the standards of proof by a specification of what constitutes grounds for the mathematical statements of the practice. We are now in a position to state precisely the ground-based account of the validity of mathematical inference: a mathematical inference (P, C, O) is uafa'd within a given mathematical prac­tice L, M, Q, R, S if and only if the operation O provides a ground for the conclusion C given grounds for the premises P, where grounds for C and P are specified by the set of metamathematical views M. The validity of mathematical inference is thus defined by components R and M together, which is in direct line with Kitcher's view:

[T]he criteria [...] for correct inference are set by the background metamathematical views [...]. Those metamathematical views are intended to specify the conditions which must be met if a sequence is to fulfil the distinctive functions of proofs. [Kitcher 1984, 180]

  • 11 We shall come back to the example of elementary Euclidean geometry in sec­tion 6.

24To illustrate the ground-based account of the validity of mathematical inference, let us consider the different examples of accepted reasonings men­tioned above. First of all, in the mathematical practice of number theory, mathematical induction leads to valid mathematical inferences since, as we have seen in the previous section, it consists in an operation that results in what is recognized as grounds for statements of the form nA(n) within this practice. For elementary Euclidean geometry, the validity of diagrammatic inferences depends on the set of metamathematical views of the considered practice: in the mathematical practice of Euclid's Elements, diagrammatic inferences yield grounds for their conclusions, while in contemporary math­ematical practice they don't. According to the ground-based account of the validity of mathematical inference, the difference lies precisely in the different specifications of what constitutes a ground for a geometrical statement in the metamathematical views of the two practices.11 Sometimes, it is a matter of discussion whether or not a given operation yields a ground for its conclusion, as witnessed by the debate around the status of the computer-assisted proof of the four-colour theorem in the mathematical practice of graph theory. In this particular case, this reflects an indeterminacy with respect to the standards of ground within the metamathematical views of the practice, and in turn an indeterminacy with respect to what constitutes a valid mathematical infer­ence. Finally, some mathematical inferences involve operations that do not yield (conclusive) grounds for their conclusions, and therefore should not be considered as valid according to the ground-based account. Numerical meth­ods or inductive generalizations are examples of such mathematical inferences in the mathematical practice of number theory.

25Following the methodology described in the introduction, we shall now spell out the notion(s) of proof gap resulting from the ground-based account of the validity of mathematical inference by investigating how one can fail to draw a valid mathematical inference in this specified sense. To this end, it will be useful to distinguish between two families of proof gaps. The reason is that, as we just saw, the validity of mathematical inference is determined by the two components R and M of a mathematical practice. Yet, mathematicians sometimes use the term proof gap to refer to situations in which some inferences within a given mathematical practice are evaluated with respect to the metamathematical views of another mathematical practice, i.e., the components R and M are taken from different practices. To distinguish between these two cases, we introduce the following terminology: if a proof gap occurs when the two components R and M are taken from the same mathematical practice, we will speak of intra-praxis gap; if a proof gap occurs when the two components R and M are taken from different mathematical practices, we will speak of inter-praxis yap. We will now investigate the different possible cases in which one can fail to draw a valid mathematical inference, focusing in turn on intra-praxis gaps and inter-praxis gaps.

5 Intra-praxis gaps

26An intra-praxis yap occurs in a mathematical proof of a given mathematical practice whenever there is a failure in drawing a valid mathematical inference, and where validity is evaluated with respect to the practice's standards of ground. The first parameter in this definition is the notion of the validity of mathematical inference, which is given in this section by the ground-based account. The second parameter is the notion of failure. The ground-based account allows for different possible interpretations of what it could mean to fail in drawing a valid mathematical inference. We now want to evaluate whether, by fixing different interpretations of the notion of failure, one is able to capture different intuitive notions of proof gap from mathematical practice. To this end, we propose in this section the following methodology. It turns out that a fine-grained taxonomy of different notions of proof gap present in mathematical practice has been proposed by Don Fallis in [Fallis 2003]. This taxonomy offers a perfect opportunity to evaluate the ground-based account, the question being: is it possible, by giving different interpretations of the notion of failure in the definition of intra-praxis gap, to capture the different kinds of proof gaps identified in [Fallis 2003]? To answer this question, we will now consider in turn the three kinds of proof gaps constitutive of Don Fallis' taxonomy—i.e., inferential yaps, enthymematie yaps and untraversed yaps— and see if they can be accounted for by identifying different interpretations of the notion of failure.

Inferential yaps are defined by Don Fallis as follows:

A mathematician has left an inferential gap whenever the partic­ular sequence of propositions that the mathematician has in mind (as being a proof) is not a proof. [Fallis 2003, 51]

27According to Don Fallis, the existence of inferential gaps corresponds to a form of fallibilism, in the sense that mathematicians might sometimes be mistaken in recognizing a sequence of mathematical inferences as a proof. Within the ground-based account of the validity of mathematical inference, such a failure can be represented as a mistaken evaluation of the result of the operation involved in one (or more) mathematical inference of the proof as constituting a ground for its conclusion. This possibility is indeed considered by Prawitz:

To say that there are deductive inferences that give rise to con­clusive and even compelling grounds or proofs is of course not to say that there are infallible roads to knowledge. One can never rule out that one is mistaken about what one thinks is a ground or a proof of a sentence. [Prawitz 2012b, 2]

28Thus, this precise notion of failure in the evaluation of what constitutes a ground for a mathematical statement allows us to capture the notion of infer­ential gap as follows: an inferential gap occurs in a mathematical proof of a mathematical practice L, M, Q, R, Swhenever there is a mathematical inference (P, C, O) in the proof such that one has mistakenly evaluated the result of the operation O, applied to grounds for the premises P, as being a ground for the conclusion C.

Enthymematie gaps are defined by Don Fallis as follows:

A mathematician has left an enthymematie gap whenever he does not explicitly state the particular sequence of propositions that he has in mind (as being a proof). [Fallis 2003, 54]

29One of the main reasons for the existence of enthymematie gaps, according to Don Fallis, is to facilitate communication: by omitting in the communication of mathematical proofs the steps that anyone can easily reconstruct from common background knowledge, one can more efficiently communicate the essential aspects of new proofs. Where is the failure located in an enthymematie gap? Importantly, the failure is not on the side of the one communicating the proof: if one leaves an enthymematie gap between some premises and a conclusion, one is supposed to have successfully obtained a ground for the conclusion given grounds for the premises, and this by having carried out the operations involved in the omitted mathematical inferences. Rather, the failure lies in the communication of the proof: an enthymematie gap occurs precisely when a mathematical inference (P, C, O) in the communicated proof is such that either the operation O does not belong to the set of accepted reasonings, or O fails to provide a ground for C given grounds for P, and such that the omitted mathematical inferences can easily be reconstructed from common background knowledge in such a way that a chain of operations from the set of accepted reasonings of the practice results in a ground for C given grounds for P. Thus, enthymematic gaps can be captured by specifying this notion of failure in communication through a three part condition: an enthymematie gap occurs in a mathematical proof of a mathematical practice L, M, Q, R, Swhenever there is a mathematical inference (P, C, O) in the proof such that (i) either the operation O does not belong to the set of accepted reasonings R, or O fails to provide a ground for C given grounds for P, (ii) the author of the proof knows a chain of mathematical inferences in R for which she has verified that the application of the sequence of operations involved yields a ground for C given grounds for P and (iii) this chain of mathematical inferences can easily be reconstructed from the common background knowledge of the agents involved in the mathematical practice L, M, Q, R, S.

Untraversed yaps are defined by Don Fallis as follows:

A mathematician has left an untraversed gap whenever he has not tried to verify directly that each proposition in the sequence of propositions that he has in mind (as being a proof) follows from previous propositions in the sequence by a basic mathematical inference. [Fallis 2003, 56-57]

30For untraversed gaps, the failure is easily identified as a failure in performance: for some mathematical inferences in a mathematical proof, one has not per­formed the associated operations and verified that they resulted in grounds for their conclusions given grounds for their premises. Untraversed gaps can then be captured in the following way: an untraversed gap occurs in a mathematical proof of a mathematical practice L, M, Q, R, Swhenever there is a mathematical inference (P, C, O) in the proof such that one has not carried out the operation O on grounds for the premises P, and a fortiori has not verified that it resulted in a ground for the conclusion C.

31Thus, the three kinds of proof gaps from Don Fallis' taxonomy can be accounted for as particular kinds of failures in drawing valid mathematical inferences, where the validity of mathematical inference is determined by the ground-based account. More specifically, inferential gaps correspond to fail­ure in evaluation, enthymematie gaps to failure in communication and untra­versed gaps to failure in performance. We shall now turn our attention to inter-praxis gaps.

6 Inter-praxis gaps

  • 12 There are many different ways in which one can understand 'different' mathe­matical practices in th (...)

32An inter-praxis gap occurs in a mathematical proof of a given mathematical practice whenever there is a failure in drawing a valid mathematical infer­ence, and where validity is evaluated with respect to a different mathematical practice's standards of ground.12 Since this definition differs from the one of intra-praxis gap by simply requiring that operations and grounds be taken from different practices, the three notions of intra-praxis gap from the previ­ous section can easily be reinterpreted as inter-praxis gap. However, none of the three resulting notions seem to correspond to an intuitive notion of proof gap from mathematical practice. Yet there is a specific kind of inter-praxis gap that is commonly mentioned in mathematical practice. Maybe one of the most illustrative examples concerns the diagrammatic inferences in Euclidean geometry, the situation being summarized by Manders as follows:

In Euclidean geometry, a diagram has standing to license infer­ence, just as do relationships recognized in the text. It is now commonly held that this is a defect of rigor. But the extraordi­nary career of Euclidean practice justifies a fuller consideration. It was a stable and fruitful tool of investigation across diverse cul­tural contexts for over two thousand years. During that time, it generally struck thoughtful and knowledgeable people as the most rigorous of human ways of knowing [...]. [Manders 2008, 81]

33In this example, we are in the presence of a family of mathematical inferences— the diagrammatic inferences—that were considered as valid in the mathemat­ical practice of Euclid's Elements [Euclid ana], but that are not considered as valid in contemporary mathematical practice. Consequently, it is now thought that diagrammatic inferences create proof gaps in the mathematical proofs of Euclid's Elements, as Manders puts it:

[I]t has been commonplace for at least the last century to castigate traditional geometry for 'gaps in arguments' [...] due to 'reading off from the figure'. [Manders 2008, 87]

  • 13 See [Kitcher 1981, 1984] for a detailed analysis of rigorization processes in math­ematical practic (...)

34What does the failure consist in for this particular kind of proof gap? This question finds a natural answer within the ground-based account of the valid­ity of mathematical inference, namely that the standards of what constitutes a ground for a mathematical statement have changed from Euclid to con­temporary mathematical practice: even though diagrammatic inferences yield (conclusive) grounds for their conclusion according to the metamathematical views of the mathematical practice of Euclid's Elements, they do not accord­ing to the metamathematical views of contemporary mathematical practice. In other words, the results of the operations involved in diagrammatic infer­ences fail to meet the standards of ground from contemporary mathematical practice, while they do meet the ones of Euclid's practice. This type of proof gap seems to occur when a process of rigorization of mathematical practice is taking place,13 and can be defined in the present framework as follows: a rigorization gap occurs in a mathematical proof of a mathematical prac­tice L, M, Q, R, S whenever there is a mathematical inference (P, C, O) in the proof such that the result of the operation O, applied to grounds for the premises P, does not constitute a ground for the conclusion C according to the metamathematical views M, but does constitute a ground for the conclusion C according to the metamatheniatical views M' of a mathematical practice prior to L, M, Q, R, S in the historical development of mathematics.

35Two important lessons can be drawn from the existence of rigorization gaps. Firstly, rigorization gaps differ from the three kinds of proof gaps con­stitutive of Don Fallis' taxonomy, since they do not correspond to failure in evaluation, communication or performance. They appear thereby as a strong candidate for extending this taxonomy. Secondly, any account of the validity of mathematical inference and of the notion of proof gap which aims to be faithful to mathematical practices past and present should be able to account for rig­orization gaps, as in the example of diagrammatic inferences in Euclidean ge­ometry. It then seems that any derivation-based account is doomed to fail this requirement as it provides a fixed point of reference—i.e., the notion of formal derivation—from which to evaluate the validity of mathematical inferences. Derivation-based accounts cannot in particular explain why diagrammatic in­ferences are considered as valid in Euclid's practice but not in contemporary mathematical practice. As we have just seen, the ground-based account offers such a flexibility and is able to account for rigorization gaps. The reason being that the two central notions of operation and ground in Prawitz's account of the validity of inference are susceptible of different interpretations, and can in particular be relativized to specific mathematical practices.

7 Conclusion

36We began this paper with the observation that a philosophical account of the common gap-based formulation of mathematical rigor requires an account of proof gap, and that an account of proof gap requires in turn an account of the validity of mathematical inference. The aim of the paper was then to evaluate two possible views of the validity of mathematical inference with respect to their capacity to yield an account of proof gap that would adequately cap­ture the intuitive notion(s) of proof gap from mathematical practice. The first view was provided by the contemporary standards of mathematical rigor which evaluate the validity of mathematical inference with respect to the notion of formal derivation. We saw that there were several possible interpretations of the relation between the notions of rigorous mathematical proof and for­mal derivation, leading to different derivation-based accounts of the validity of mathematical inference. We then argued that none of the resulting derivation-based accounts of proof gap adequately capture the intuitive notion(s) of proof gap from mathematical practice. The second view was based on a recent ground-based account of the validity of inference proposed by Prawitz. We first specified Prawitz's account to mathematical inference by integrating the notions of operations and grounds within Kitcher's notion of mathematical practice. In order to evaluate the resulting ground-based account of proof gap, we attempted to describe several intuitive notions of proof gap as par­ticular types of failure in drawing valid mathematical inferences, where the validity of mathematical inference was specified by the ground-based account. Our analysis has revealed that several intuitive notions of proof gap can be accommodated in this way within this framework. More precisely, we saw how the three kinds of proof gaps comprising Don Fallis' taxonomy—inferential gaps, enthymematic gaps and untraversed gaps—can be represented respec­tively as failure in evaluation, communication and performance. We also saw that the ground-based account was particularly suitable for representing what we called rigorization gaps, a particular kind of proof gap that occur from a (temporal) cross-perspective on different mathematical practices. Finally, we noticed that rigorization gaps constitute a serious challenge for any derivation-based account of proof gap. We shall then conclude that the ground-based account offers a promising framework for representing different intuitive no­tions of proof gap present in mathematical practice, and therefore should be of particular interest for the philosophy of mathematical practice.

37Yet, a full development of the ground-based account faces several impor­tant challenges. Some of them have already been raised in critical responses to Prawitz in [Pagin 2012] and [Murzi 2011]. Pagin identifies two problems [Pagin 2012, 881]: the first one being that the ground-based account does not fit the inferential practice of ordinary speakers; the second one that the ground-based account requires a reflection principle saying that when an agent is in possession of a ground for a statement she must be aware of it, which according to Pagin leads to problematic consequences. From the point of view of moderate inferentialism, Murzi raises two concerns [Murzi 2011, 289]: the first one regarding the unclear metaphysical nature of grounds; the second one regarding problematic consequences of conceiving the meaning of a statement as determined by what counts as a ground for it. This last point is probably the most pressing challenge facing the development of a ground-based account of the validity of mathematical inference. More specifically, such an account requires that if one understands the meaning of the mathematical statements involved in a given mathematical inference, one has the capacity to recognize what constitutes a ground for them. We shall then provide a full specifica­tion of (i) what constitutes a ground for a mathematical statement, and (ii) how one recognizes whether something counts as a ground for a mathematical statement. As we saw, Prawitz's response to this challenge is to adopt a the­ory of meaning in which the meaning of a statement is determined by what counts as a ground for holding the statement true, but this solution raises a number of problems as noticed in [Murzi 2011]. Can a ground-based theory of meaning for mathematical statements be developed along Prawitz's line while avoiding such problems? Is there an alternative way to specify what constitutes a ground for a mathematical statement? How can we account for one's capacity to recognize what counts as a ground for a mathematical statement? Addressing these questions is the next step towards a full development of a ground-based account of mathematical rigor, proof gap and the validity of mathematical inference.

Haut de page

Bibliographie

Antonutti Marfori, Marianna [2010], Informal proofs and mathematical rigour, Studio, Logica, 96(2), 261-272.

Avigad, Jeremy, Donnelly, Kevin, Gray, David, & Raff, Paul [2007], A formally verified proof of the prime number theorem, ACM Transactions on Computational Logic (TOOL), 9(1), 1-23.

Azzouni, Jody [2004], The derivation-indicator view of mathematical practice, Philosophia Mathematica, 12(2), 81-106.

Detlefsen, Michael [2009], Proof: Its nature and significance, in: Proof and Other Dilemmas: Mathematics and Philosophy, edited by B. Gold & A. Simons, R. Washington, D.C.: The Mathematical Association of America, 3-32.

Euclid [ana], The Thirteen Books of Euclid's Elements.

Fallis, Don [2003], Intentional gaps in mathematical proofs, Synthese, 134(1), 45-69.

Kitcher, Philip [1981], Mathematical rigor-Who needs it?, Nous, 15(4), 469-493.
[1984], The Nature of Mathematical Knowledge, New York: Oxford

University Press.

Leitgeb, Hannes [2009], On formal and informal provability, in: New Waves in Philosophy of Mathematics, edited by 0. Linnebo & O. Bueno, New York: Palgrave, Macmillan, 263-299.

Mac Lane, Saunders [1986], Mathematics: Form and Function, New York: Springer-Verlag.

Mancosu, Paolo [2008], The Philosophy of Mathematical Practice, Oxford: Oxford University Press.

Manders, Kenneth [2008], The Euclidean diagram, in: Philosophy of Mathematical Practice, edited by P. Mancosu, Oxford: Oxford University Press, 80-133.

Murzi, Julien [2011], Inferentialism without verificationism: Reply to Prawitz, in: Logic and Knowledge, edited by C. Cellucci & E. Ippoliti, Cambridge: Cambridge Scholars Publishing, 285-290.

Pagin, Peter [2012], Assertion, inference, and consequence, Synthese, 187(3), 869-885.

Pierpont, James [1928], Mathematical rigor, past and present, Bulletin of the American Mathematical Society, 34, 23-53.

Prawitz, Dag [2009], Inference and knowledge, in: Logica Yearbook 2008, edited by M. Pelis, London: College Publications, 175-192.
− [2012a], The epistemic significance of valid inference, Synthese, 187(3), 887-898.
− [2012b], Validity of inference, in: Proceedings from the 2nd Launer Symposium on the Occasion of the Presentation of the Launer Prize at Bern 2006, (to appear).

Rav, Yehuda [1999], Why do we prove theorems?, Philosophia Mathematica, 7(1), 5-41.

Robinson, John Alan [1997], Informal rigor and mathematical understand­ing, in: Computational Logic and Proof Theory, Heidelberg & New York: Springer, Proceedings of the 5th annual Kurt Godel Colloquium, August 25-29, 1997, 54-64.

van Kerkhove, Bart & van Bendegem, Jean Paul (eds.) [2010], Perspectives on Mathematical Practices: Bringing Together Philosophy of Mathematics, Sociology of Mathematics, and Mathematics Education, Logic, Epistemology and the Unity of Science, Dordrecht: Springer.

Haut de page

Notes

1 See for instance Kitcher: "central to the idea of rigorous reasoning is that it should contain no gaps" [Kitcher 1981, 469].

2 We do not claim that this formulation exhausts the notion of mathematical rigor, nor are we trying to evaluate it in this respect. Our standpoint in this paper is rather to start from this common formulation of mathematical rigor and to analyze what is required to determine a philosophical account of it.

3 This observation has been used to argue that "rigor and formalization are independent concerns" [Detlefsen 2009, 17], but also to argue that the prevailing view of mathematical rigor yields an implausible account of mathematical knowledge [Antonutti Marfori 2010]. This observation is also at the basis of recent discussions on the relation between formal and informal proofs (e.g., see [Azzouni 2004], [Leitgeb 2009], [Rav 1999]).

4 This view is expressed for instance by Mac Lane: "In practice, a proof is a sketch, in sufficient detail to make possible a routine translation of this sketch into a formal proof [Mac Lane 1986, 377].

5 This point has been acknowledged by Robinson, one of the main figures in automated theorem proving, who said of the activity of formalization that: "[l]n most cases it requires considerable ingenuity, and has the feel of a fresh and separate mathematical problem in itself. In some cases [...] formalization is so elusive as to seem to be impossible" [Robinson 1997, 54].

6 For some historical examples of changes in mathematical rigor, see [Kitcher 1981], [Pierpont 1928].

7 We will come back to this point at the end of section 6.

8 In this section, when we will use the term inference, we will always refer to deductive inference.

9 A formal description of this operation has been proposed by Prawitz in [Prawitz 2012a, 897].

10 As also noted by Pagin: "A main point of Prawitz's discussion [...] is that it does not solely apply to formal systems of deduction, but to informal deductive reasoning as well" [Pagin 2012, 875].

11 We shall come back to the example of elementary Euclidean geometry in sec­tion 6.

12 There are many different ways in which one can understand 'different' mathe­matical practices in the definition of inter-praxis gap. For instance, one may compare mathematical practices from different domains (number theory, analysis, algebra, etc.), but also from the same domain but different perspectives such as the ones of pure and applied mathematics. In this section, we focus in particular on practices that differ along a temporal dimension—i.e., different mathematical practices from the same domain, but from different times in the historical development of mathe matics. Providing a taxonomy of the different possible kinds of inter-praxis gaps is beyond the scope of this paper.

13 See [Kitcher 1981, 1984] for a detailed analysis of rigorization processes in math­ematical practice.

Haut de page

Pour citer cet article

Référence électronique

Yacin Hamami, « Mathematical Rigor, Proof Gap and the Validity of Mathematical Inference », Philosophia Scientiæ [En ligne], 18-1 | 2014, mis en ligne le 15 mars 2017, consulté le 24 juin 2018. URL : http://journals.openedition.org/philosophiascientiae/908 ; DOI : 10.4000/philosophiascientiae.908

Haut de page

Auteur

Yacin Hamami

Centre for Logic and Philosophy of Science Vrije Universiteit Brussel (Belgium)

Haut de page

Droits d’auteur

Tous droits réservés

Haut de page