Proofs as deduction from explicitly stated postulates was conceived by the Greeks. It was connected with the axiomatic method. Since Plato, Aristotle and Euclid the axiomatic method was considered as the best method to justify and to organize mathematical knowledge. The first mature and most representative example of its usage in mathematics was the Elements of Euclid. They established a pattern of a scientific theory and in particular a paradigm in mathematics. Since Euclid till the end of the 19th century, mathematics was developed as an axiomatic – in fact rather a quasi-axiomatic – theory based on axioms, postulates and definitions. Axioms were principles common to all sciences, postulates – specific principles taken for granted by a mathematician engaged in the demonstration of theorems in a particular domain. Definitions should provide meaning to new notions – in practice definitions were rather explanations of notions than proper definitions in the strict sense, moreover, they were explanations in the unprecise everyday colloquial language. Note that the language of a theory was not separated from the natural language. Proofs of theorems contained several gaps – in fact the lists of axioms and postulates were not complete; one freely used in proofs various “obvious” truths or referred to the intuition. Consequently, proofs were only partially based on axioms and postulates. In fact proofs were informal and intuitive, they were rather demonstrations and the very concept of a proof was of a psychological and sociological (and not of a logical) nature.
Note that the language of theories was simply the unprecise colloquial language. Till the end of the 19th century, mathematicians were convinced that axioms and postulates should be true statements, hence sentences describing the real state of affairs (in the mathematical reality).22 It seems to be connected with Aristotle’s view that a proposition is demonstrated (proved to be true) by showing that it is a logical consequence of propositions already known to be true. Demonstration was conceived here of as a deduction whose premises are known to be true, and a deduction was conceived of as a chaining of immediate inferences.
It should be noted that Euclid’s approach (connected with Platonic idealism) to the problem of the development of mathematics and the justification of its statements (which found its fulfilment in the Euclidean paradigm), i.e. justification by deduction (by proofs) from explicitly stated axioms and postulates, was not the only approach and method which was used in the ancient Greek (and later). The ←38 | 39→other one (call it heuristic) was connected with Democritus’ materialism. It was applied, e.g., by Archimedes who used in his mathematical works not only deduction but any methods, such as intuition or even experiments (not only mental ones) to solve problems. One can see this, e.g., in his considerations concerning the calculation of the volume of a sphere using cylinder with two excavated cones or in his quadrature of the parable.
Though the Euclidean approach won and dominated in the history, one should note that it formed rather an ideal and not the real scientific practice of mathematicians. In fact rigorous, deductive mathematics was rather a rare phenomenon. On the contrary, intuition and heuristic reasoning were the animating forces of mathematical research practice. The vigorous but rarely rigorous mathematical activity produced “crises” (e.g. the Pythagoreans’ discovery of the incommensurability of the diagonal and the side of a square, Leibniz’s and Newton’s problems with the explanation of the nature of infinitesimals, Fourier’s “proof ” that any function is representable in a Fourier series, antinomies connected with Cantor’s imprecise and intuitive notion of a set).
New elements appeared in the 19th century with the trend whose aim was the clarification of basic mathematical concepts, especially those of analysis (cf. works by Cauchy, Weierstrass, 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