The formalist point of view maintains that formal derivations underlying proofs, although usually not carried out in practice, contribute to the confidence in mathematical theorems. Opposing this opinion, the main claim of the present paper is that such a gain of confidence obtained from any link between proofs and formal derivations is, even in principle, impossible in the present state of knowledge. Our argument is based on considerations concerning length of formal derivations. Thanks to Jody Azzouni for enlightening discussions concerning (...) the subject of this paper and to anonymous referees whose important remarks permitted us to correct the arguments and improve presentation. The remaining flaws remain, of course, solely the responsibility of the author. This research was partially supported by NSERC discovery grant and by the Research Chair in Distributed Computing at the Université du Québec en Outaouais. CiteULike Connotea Del.icio.us What's this? (shrink)

Kant discovered a philosophical problem with mathematical proof. Despite being a priori , its methodology involves more than analytic truth. But what else is involved? This problem is widely taken to have been solved by Frege’s extension of logic beyond its restricted (and largely Aristotelian) form. Nevertheless, a successor problem remains: both traditional and contemporary (classical) mathematical proofs, although conforming to the norms of contemporary (classical) logic, never were, and still aren’t, executed by mathematicians in a way that transparently reveals (...) why these proofs—written in the vernacular to this very day—succeed in conforming to those norms. (shrink)

Ordinary mathematical proofs—to be distinguished from formal derivations—are the locus of mathematical knowledge. Their epistemic content goes way beyond what is summarised in the form of theorems. Objections are raised against the formalist thesis that every mainstream informal proof can be formalised in some first-order formal system. Foundationalism is at the heart of Hilbert's program and calls for methods of formal logic to prove consistency. On the other hand, ‘systemic cohesiveness’, as proposed here, seeks to explicate why mathematical knowledge is (...) coherent and places the problem of reliability within the province of the philosophy of mathematics. (shrink)

Derivationists, those wishing to explain the correctness and rigour of informal proofs in terms of associated formal proofs, are generally held to be supported by the success of the project of translating informal proofs into computer-checkable formal counterparts. I argue, however, that this project is a false friend for the derivationists because there are too many different associated formal proofs for each informal proof, leading to a serious worry of overgeneration. I press this worry primarily against Azzouni's derivation-indicator account, but (...) conclude that overgeneration is a major obstacle to a successful account of informal proofs in this direction. (shrink)

I focus on three preoccupations of recent writings on proof. -/- I. The role and possible effects of empirical reasoning in mathematics. Do recent developments (specifically, the computer-assisted proof of the 4CT) point to something essentially new as regards the need for and/or effects of using broadly empirical and inductive reasoning in mathematics? In particular, should we see such things as the computer-assisted proof of the 4CT as pointing to the existence of mathematical truths of which we cannot have a (...) priori knowledge? -/- 2. The role of formalization in proof. What are the patterns ofinference according to which mathematical reasoning naturally proceeds? Are they of 'local' character (i.e. sensitive to the subject-matter of the reasoning concerned) or 'global' character (i.e. invariant across all subject-matters)? Finally, what if any relationship is there (a) between the patterns of inference manifest in a proof and its explanatory capacity and (b) between explanatory capacity and rigor? -/- 3. Diagrams and their role in mathematical reasoning. What essentially is diagrammatic reasoning, and what is the nature and basis of its usefulness? Can it play a justificative role in the development of mathematical knowledge and, more particularly, in genuine proof? Finally, does the use of diagrammatic reasoning force an adjustment either in our conception of rigor or in our view of its importance? (shrink)

The form of nominalism known as 'mathematical fictionalism' is examined and found wanting, mainly on grounds that go back to an early antinominalist work of Rudolf Carnap that has unfortunately not been paid sufficient attention by more recent writers.

Ordinary mathematical proofs—to be distinguished from formal derivations—are the locus of mathematical knowledge. Their epistemic content goes way beyond what is summarised in the form of theorems. Objections are raised against the formalist thesis that every mainstream informal proof can be formalised in some first-order formal system. Foundationalism is at the heart of Hilbert's program and calls for methods of formal logic to prove consistency. On the other hand, ‘systemic cohesiveness’, as proposed here, seeks to explicate why mathematical knowledge is (...) coherent (in an informal sense) and places the problem of reliability within the province of the philosophy of mathematics. (shrink)

The heuristics and strategies presented in Lakatos' Proofs and Refutations are well-known. However they hardly present the whole story as many authors have shown. In this paper a recent, rather spectacular, event in the history of mathematics is examined to gather evidence for two new strategies. The first heuristic concerns the expectations mathematicians have that a statement will be proved using given methods. The second heuristic tries to make sense of the mathematicians' notion of the quality of a proof.

In this paper, we discuss the prevailing view amongst philosophers and many mathematicians concerning mathematical proof. Following Cellucci, we call the prevailing view the “axiomatic conception” of proof. The conception includes the ideas that: a proof is finite, it proceeds from axioms and it is the final word on the matter of the conclusion. This received view can be traced back to Frege, Hilbert and Gentzen, amongst others, and is prevalent in both mathematical text books and logic text books.

There are two distinct meanings to ‘mathematical proof’. The connection between them is an unsolved problem. The first step in attacking it is noticing that it is an unsolved problem.

In Section 2, I survey some of the ways that computers are used in mathematics. These raise questions that seem to have a generally epistemological character, although they do not fall squarely under a traditional philosophical purview. The goal of this article is to try to articulate some of these questions more clearly, and assess the philosophical methods that may be brought to bear. In Section 3, I note that most of the issues can be classified under two headings: some (...) deal with the ability of computers to deliver appropriate “evidence” for mathematical assertions, a notion that is explored in Section 4, while others deal with the ability of computers to deliver appropriate mathematical “understanding,” a notion that is considered in Section 5. Final thoughts are provided in Section 6. (shrink)

The relationship is explored between formal derivations, which occur in artificial languages, and mathematical proof, which occurs in natural languages. The suggestion that ordinary mathematical proofs are abbreviations or sketches of formal derivations is presumed false. The alternative suggestion that the existence of appropriate derivations in formal logical languages is a norm for ordinary rigorous mathematical proof is explored and rejected.