Bolzano, Dedekind). Still another factor was the discovery of antinomies, in particular in set theory (C. Burali-Forte, G. Cantor, B. Russell) and of the semantical antinomies (G.D. Berry, K. Grelling). They forced the revision of some basic ideas of mathematics. Among formulated proposals was the foundational program of David Hilbert and his Beweistheorie. Note that “this program was never intended as a comprehensive philosophy of mathematics; its purpose was instead to legitimate the entire corpus of mathematical knowledge” (Rowe 1989, p. 200).
The main role in Hilbert’s program was played by formal (or formalized) proofs. This device was introduced on the basis of (and thanks to) the mathematical logic developed in the 19th century, in particular on the basis of the work of Gottlob Frege who constructed the first formalized system – it was the system of propositional calculus based on two connectives: negation and implication. Investigations carried out in the framework of Hilbert’s program established the new scientific discipline, i.e. the metamathematics.
Recall that the concept of a formal proof must be related to a given formal theory. To express such a theory one should at the beginning fix its language. The rules of forming formulas in it should have strictly formal and syntactic character – only the shape of symbols can be taken into account and one should entirely abstract from their possible meaning or interpretation. Next one fixes axioms (logical, non-logical and usually identity axioms) and rules of inference. The latter must have entirely syntactic and formal character. A formal proof of a statement (formula) φ ←39 | 40→is now a finite sequence of formulas in the given language φ1,φ2,φ3, . . . ,φn such that the last member of the sequence is the formula φ, and all members of it either belong to the set of presumed axioms or are consequences of previous members of the sequence according to one of the accepted rules of inference. Observe that this concept of a formal proof has a syntactic character and does not refer to any semantical notions such as meaning or interpretation.
As a result of the described development, one has to deal nowadays in mathematics with at least two concepts of a proof: the formal one, used mainly by logicians and specialists in metamathematics in the foundational studies as well as by computer scientists (cf. modern theorem provers), and on the other hand the “normal”, “usual” concept of a proof used in mathematical research practice. What are the relations between them? Is the metamathematical concept a precise explication of the “everyday” concept? Do they play similar roles in mathematics or not? To what extent does the concept of a formal proof reflect the main features and the nature of an informal proof used by mathematicians in their researches?
Informal proofs and their role
Mathematics was and is developed in an informalway using intuition and heuristic reasonings – it is still developed in fact in the spirit of Euclid (or sometimes of Archimedes) in a quasi-axiomatic way. Moreover, informal reasonings appear not only in the context of discovery but also in the context of justification. Any correct methods are allowed to justify statements. But what does it mean “correct”? In the research practice, this was and is decided by the community of mathematicians. Consequently, the criteria of being correct have been changing in the history and in the process of developing mathematics. The concept of proof was and is in fact not an absolute notion but it was and is culturally and sociologically dependent and motivated; it had and has cultural and sociological components. The main aim of a mathematician is always to convince the audience that the given result is justified, correct and true (the latter concept being used in an intuitive and vague way) and not to answer the question whether it can be deduced from stated axioms. In the research practice, a proof is in fact an argumentation that should indicate the correctness of a claimed thesis – in particular its form depends on and is relative to a background knowledge of those to whom the proof is presented. And here appears a psychological moment in the understanding and functioning of proofs.
The ultimate aim of mathematics is “to provide correct proofs of true theorems” (Avigad 2006, p. 105). In their research practice, mathematicians usually do not distinguish concepts “true” and “provable” and often replace them by each other. Mathematicians used to say that a given theorem holds or that it is true and not that it is provable in such and such theory. In fact, they do not distinguish concepts “true” and “provable” and often replace them by each other, Add that axioms ←40 | 41→of theories being developed are not always precisely formulated and admissible methods precisely described.
Proofs play various roles in the mathematical research practice. One can distinguish (cf. CadwalladerOlsker 2011; De Villiers 1999) among others the role of: (1) verification, (2) explanation, (3) systematization, (4) discovery, (5) intellectual challenge, (6) communication and (7) justification of definitions.
The most familiar to research mathematicians is the role of verification. A statement can be treated as belonging to the body of mathematics only when it has been verified. The proof should not only show that a given sentence is true and holds but should also explain why it is true and holds. This role explains why mathematicians are often looking for new proofs of known theorems – newproofs should have more explanatory power. The role of systematization was exemplified already by Euclid’s Elements. In this work, many theorems known to Greeks have been collected and organized in such a way that they followed from axioms, postulates, definitions and previously proved theorems. It was shown in this way that the accepted axioms, postulates and definitions form a sufficient base on which the whole edifice of mathematics can be developed. Note that the role of discovery may be – prima facie – rather seldom associated with proofs but it is not excluded. In fact, e.g. non-Euclidean geometries were arrived at through purely deductive means. Recall that since Euclid one asked the question whether the fifth postulate on parallels formulated in Elements is independent of other axioms and postulates or can be deduced from them. After several attempts undertaken through the centuries, it has been shown in the 19th century that it is reasonable to consider systems of geometry in which the negation of the fifth postulate is assumed instead of the fifth postulate itself, and it is possible to show that such systems are consistent.
Finding proofs is the intellectual challenge for mathematicians: there is a theorem – we want to prove it. Proofs serve in the community of mathematicians as communication means. They communicate not only the reasons why a given statement is a true theorem but introduce also new methods which can be used sometimes in other domains. Proofs can provide also justification of definitions.
The most important roles played by proofs in the research mathematical practice are of course verification and explanation. Note that a proof that verifies a theorem does not have to explain why it holds. One can distinguish between proofs that convince and proofs that explain. The former should show that a statement holds or is true and can be accepted, the latter – why it is so. Of course, there are proofs that both convince and explain. The explanatory proof should give an insight in the matter whereas the convincing one should be concise or general. One can distinguish also between explanation and understanding. Mathematicians←41 | 42→often treat simplicity as a characteristic feature of understanding. Observe that, as G.-C. Rota writes in (1997, p. 192):
[i]t is an article of faith among mathematicians that after a new theorem is discovered, other, simpler proof of it will be given until a definitive proof is found.
In this context, it is worth distinguishing between unveiling proofs and consolidating ones. The former one is “a proof which proves a theorem which was unknown before” and the latter is “a proof of a theorem which is already known to be true” (Kahle 2015). Proofs of the second type do not contribute to the truth of a theorem – they consolidate our knowledge of this truth. Such a proof can be quite different from the original one. Aschbacher wrote about this phenomenon in the following way (2005, p. 2403):
The first proof of a theorem is usually relatively complicated and unpleasant. But if the result is sufficiently important, new approaches replace and refine the original proof, usually by embedding it in a more sophisticated conceptual context, until the
