Abstract: This paper is an attempt to review the historically existing types of demonstration of mathematical theorems. The author shows how the notion of mathematical proof changed throughout time from the moment when mathematicians had realized (thanks to the philosophical method) the necessity to justify their theses until a precise notion of a proof appeared in the framework of the formal method.

Nicolas Bourbaki¹ - the author of a treatise which reviews the whole mathematics of our century, in the second sentence of the introduction to Book I, Chapter I, of his monumental work The Elements of Mathematics, wrote: "what was a proof for Euclid remains a proof for us".² Perhaps it was an expression of his belief in the unity of mathematics throughout ages, perhaps an expression of his respect for the greatness of Euclid himself, nevertheless this declaration taken literally is evidently untrue. Bourbaki's style of practising mathematics, because of its absolute accuracy, exceeds the canons known and practised by Euclid. Euclid, for instance, used some notions which he didn't define, treating them as evident; the system of axioms of his geometry was incomplete and his proofs usually enthymematic. Although some analogies, connected not only with the title, can be found between these works, as regards the problem of the proof, more than an epoch separates both treatises. It is a result of a 'revolution' which follows from the formalization of mathematics.

Mathematics is commonly perceived as a 'kingdom' of precision, and mathematical theorems as absolute truth in the sense that, once proved, they are considered true forever. It seems, however, that such a picture is a significant simplification, it is an idealization of the historically existing demonstration procedures. Contrary to appearances, just as in many empirical disciplines when verifying their achievements along with the new discoveries or methodological changes, it was also in the case of mathematics that 'good' proofs happened to be undermined, commonly acknowledged proofs to be rejected and unquestioned proofs sometimes disappeared together with philosophical conceptions. For example, the Pythagoreans considered as precise only the arithmetic proofs - the arithmetic intuition was a criterion of correctness. Soon, however, the first crisis of the foundations of mathematics - the discovery of the irrational numbers, or to be more specific, the incommensurability of some line segments with a given one, led to the loss of faith in the certainty of arithmetic reasoning. The solution of this crisis is connected with the proposal made by Eudoxos. Along with his program of geometrization of arithmetic, geometric intuition gains its significance. This trend in the development of mathematics reached its peak already in antiquity in the Elements by Euclid. This work was considered for ages a pattern to be followed, however, a more precise and critical contemporary analysis has shown that it is not devoid of inaccuracies and gaps. What was precisely proved for Euclid, wasn't precisely proved for Descartes or Leibniz. Their proofs didn't satisfy Cauchy or Weierstrass who, in turn, didn't appear to be satisfactorily precise for Russell and Hilbert. Thus, the history of mathematics doesn't confirm the conviction about the existence of the timeless contents of the notion of mathematical proof. Let's trace how it developed throughout ages.

Let's deal with the essence of mathematical demonstration first. The emergence of a proof is closely connected with the 'birth' of the very mathematics. It can be said that mathematics arose together with the appearance of the idea of a proof.³ To put it shortly, this idea in turn is, as I think, the result of the application by the ancient Greek philosophers of a discourse about the method, which arose on the philosophical background, to the practical abilities connected with calculating and measuring, worked out in the ancient civilizations of Sumer, Babylon and Egypt. As a result of this process, the ancient thinkers realized that there appeared a need to justify, not only to notice, that for instance, a diameter divides a circle into two equal parts. It was already most probably Tales and definitely Pythagoras who realized the need to prove the formulated theorems in such a way that an average sane mortal could accept them.⁴

Such reasoning, one would think unnecessary from the point of view of practical applications, led to an emergence of a new discipline of science - mathematics. Developing first in the framework of philosophy, mathematics soon became an independent science, possessing its subject matter and method. We can attribute its magnificent development not only to philosophical influences but also to inspirations of religious nature (by which I mean Pythagorean influences) and the unique Greek invention in the social sphere i.e. the democratic state system (enabling discussions and thus forcing the necessity to establish the true state of the matter in order to convince the opponents). In antiquity, thanks to the focus on the problem of demonstration procedures, mathematicians were less and less interested in the applications. Mathematics started to develop autonomously, transforming itself into a theoretical science dealing with ideal objects.

Until the XIX century - maintains Alfred Tarski - the notion of a proof had had mainly a psychological character. The proof was perceived as a mental activity which was to convince oneself or others about the truth of the considered sentence. Especially, that the considered sentence must be accepted as true if formerly some other sentences were accepted as true. The reasoning used in proofs was to be intuitively convincing, but besides, no restrictions were imposed.⁵ Let's add to Tarski's remarks that in this period mathematicians confined themselves to the semantic proofs i.e. proofs such that they argue about notions which are already interpreted (in fact, they confine themselves to arithmetic and geometry). Among the semantic proofs we can distinguish the intuitive-psychological ones, constructive ones, and mathematical experiments.

The first kind of proof consisted in argumentation basing itself on some truths commonly accepted as evident (up to Euclidean times, not even mentioned explicitly), and it was also based on the assumption of the general intelligibility of the applied notions. Such were the proofs of the well - known and famous theorems of antiquity like the theorem that: in a right angle triangle the area of a square built on the side opposite to the right angle equals the sum of the areas of the squares built on the sides adjacent to the right angle, which was ascribed to Pythagoras⁶, or the theorem about the existence of infinitely many prime numbers, formulated and proved by Euclid in his famous Elements.⁷ This type of proof is common in mathematical practice even nowadays, wherever there is no place, time or need to present a complete - in the light of contemporary requirements - proof of the presented thesis.

Constructive proofs, in turn, pointed to definite procedures allowing to solve a given problem, either concerning the existence of some objects, or of some identities, congruences, etc. These were the most frequent proofs used in ancient times, connected with the construction tasks, allowing only to use compasses and a ruler (without a scale). Whole treatises were devoted to such problems. For example, Apollonius from Perga (around 260 - 170) undertook a widespread research into problems like the following one: Let be given straight lines a and b and, on them, points A and B. Find such a straight line which would pass through a point C and would cross the former lines at A₁ and B₁ so that the proportion AA₁ :BB₁ would have a required value.

On the other hand, a mathematical experiment is such a form of justifying theorems, which cannot be reduced to logical derivations from the initial assumptions; we carry out definite operations having the character of abstract manipulations on certain objects and then we interpret them drawing conclusions or we generalize the result by induction. The reasoning proposed by Cauchy to justify Euler's theorem: In every convex polyhedron the sum of the number of the walls S and the number of the vertexes W is twice as big as the number of its edges K, i.e. S + W - K = 2, can be an example of such a mathematical experiment. Let's present shortly the idea of his reasoning to understand better this form of justification. Cauchy proposes to assume that the examined convex polyhedron is extensible in such a way that after removing one of its walls we can extend it on the plane - deforming it but without losing its walls, edges or vertexes. Having removed one wall, our formula for this flat network can be presented as follows: S + W - K = 1. Next Cauchy proposes to divide the deformed network of the polyhedron into deformed triangles as well. Let's notice that every added diagonal increases equally both the set of the edges K and the set of walls S, so that the expression S + W - K doesn't change. When we next start removing the triangles, in each case we either remove one edge, thus removing one wall - the expression S + W - K doesn't change, or we remove two edges and one vertex which causes the elimination of one wall - the expression S+ W- K doesn't change again. At the very end of this reasoning procedure, which we have called a mathematical experiment, there is left one triangle, for which the expression S + W - K = 1 applies. Let's notice, that this reasoning can be used with any convex polyhedron; therefore Euler's theorem can be considered as justified.⁸

The reasoning procedures of all the semantic proofs use intuition, appeal to imagination or common sense. In almost all without an exception (from some point of view⁹, in fact in all), there are many hidden assumptions. Then these are enthymematic proofs where not only the hidden assumptions are important but also the absent ones, as they could be arbitrarily chosen.¹⁰ Such proofs use everyday language, enriched by mathematical terms, hence it possesses all the properties of the everyday language. It is polysemous and ambiguous, frequently appealing to unclear terms. The consequence of this state of the matter is that the semantic proofs use both mathematical and extramathematical categories such as cut, deformation, movement. Besides, the frequent procedure used in semantic proofs is to appeal to extralogical factors - among others to the impression of obviousness, clearness, intuitive understanding. Moreover, in such proofs there appear gaps in the sequences of logical conclusions (we say then that these proofs don't constitute a logical continuum). In connection with the above, from the point of view of the contemporary standards of justification, the proofs of the contents type are not proofs sensu stricto.

The above characteristics of the semantic proofs is a view from the peak of the contemporary state of the metamathematical research. However, up to XIX century, mathematics was conceived as the domain of objective truth, and the semantic proofs as credible. Mathematicians in majority were convinced that their proofs uncovered absolute truths and in this sense, for them, mathematics had the features of an episteme (foundation). They thought that the theorems of mathematics should be clear and directly accessible for intuition, because they contact truth without any mediation, at least in theory. Despite many 'revolutions of precision' - by Euclid, Descartes, Cauchy or Weierstrass, this state of the matter lasted until the axiomatic theories appeared.

To tell the truth, the very belief in the absoluteness of mathematics had been undermined earlier - the reason was the emergence of non-Euclidean geometries - however, the character of a mathematical proof didn't change immediately. Only thanks to the axiomatization of arithmetic by Peano and the new precise axiomatization of geometry proposed by Hilbert, and in particular, with the axiomatization of the set theory - considered as the new foundation for the whole mathematics, a breakthrough occurred in the demonstration process. The proof of a theorem began to be considered as the derivation of the consequences of the formerly accepted axioms. We can ask the question: what is crucial in posing the problem in this way if, already a long time ago, in his work Euclid used to prove his theorems on the basis of axioms? However, in relation to what Euclid proposed, there is a little difference, which is extraordinarily rich in consequences for the considered issue. Euclid's proofs, although they are based on axioms, are semantic proofs, as Euclid only catalogued the truths which were obvious for the ancient, and he enumerated them expressis verbis as axioms and postulates. The axioms of the contemporary mathematical theories, in turn, don't have to and most frequently are not either obvious or intuitive or true in classical sense (i.e. referring to "something"). Instead, they have to meet other conditions, such as: consistency, completeness and (eventually) independence. Demonstration based on some arbitrarily chosen sentences, the so-called semi-formal proof, is methodologically radically different from the semantic proof. The proof ceases to be regarded as an argument which directly concerns the only and unconditioned truth, and becomes a simple derivation procedure of the type: if we accept some axioms, then we can derive from them such and such theorems. Semi-formal proofs are carried on by means of explicitly enumerated axioms, but they don't possess precisely coded rules of interference. The demonstration procedure appeals to intuition and understanding of primitive terms, has creative character and at its basis has a set of convictions - what is and what is not allowed while proving a theorem. This set of convictions contains, for example, the range of the permissible means of reasoning, the choice of the objects which can be used and the way of operating on these objects. Such kind of objects appeared first in the construction of non-Euclidean geometries, and in the earlier versions of the set theories, for instance in the theory of Zermelo.

Let's notice that the appearance of non-Euclidean geometries can be interpreted as the result of the considerations of the type: what geometrical theorems will we achieve, if we introduce in the set of axioms - instead of Euclid's V postulate - its negation? Viewing the case historically, mathematicians wanted to eliminate the fifth postulate by deriving it from the remaining four; when the attempts to do it directly were not successful, there were attempts to achieve contradiction by drawing conclusions from the first four and negating the fifth postulate. In this way a number of new theorems was achieved, which later led to a new theory because, to the astonishment of most mathematicians, contradiction couldn't be achieved.

On the ground of the set theory, the idea of the traditional proof was shaken by the case of appearance and application of a controversial axiom called the axiom of choice in demonstration procedures. It states that for an arbitrary family of pair-disjunctive, non-empty sets, there exists a set which contains one and only one element of each set. Not everybody accepts this axiom, but it isn't universally rejected, either, so mathematicians always make an explicit remark whether a given theorem can be proved with or without the application of this axiom. The consequences of using this axiom are so great that mathematicians don't want and can't simply renounce to it; therefore they modify the hitherto existing notion of a proof as a procedure of reaching truth, and comprehend it as a hypothetical-deductive reasoning. This fact is a confirmation of an approach to the problem of demonstration in mathematics, rather different from the traditional one.

The consolidation of this kind of approach to the problem of demonstration is strengthened by the fact that Cantorian set theory is a very rich theory which introduces the notion of actual infinity, the notion of various cardinal numbers of infinite sets, and at the same time makes an intuitive use of the law of tertium non datur, or of the previously mentioned axiom of choice. When considering finite sets, all this is justified by the intuitiveness of the procedure, whereas in case of infinite sets it can lead to ineffective (non-constructive) proofs. More precisely, I mean here that ineffective are those existential proofs having the property that some of the postulated objects, whose existence we use in these theorems, can be neither constructed nor indicated. In mathematics it is often so that we want to have a guarantee of the existence of a mapping satisfying some requirements, or of the existence of a solution of some given equation, even when we cannot or don't have to determine it precisely. Brouwer's theorem about the existence of a fixed point is an example of an existential and non-constructive mathematical result: If B is a closed sphere in n-dimensional space Rⁿ , and T : Bⁿ ® Bⁿ is a continuous mapping, then there exists a point x₀ Î Bⁿ such that T(x₀) = x₀.

Another, more intuitive example of the same type is a particular case of a theorem concerning a continuous function possessing Darboux's property: If a real function f is continuous in a closed interval < x₁,x₂ > , and the values of the function at the end points of the interval: f(x₁), f(x₂) have different signs, i.e [f(x₁)* f(x₂)] < 0, then there exists a point
x₀ Î < x₁,x₂ > such that the function has zero value in it, that is f(x₀) = 0.

Indirect proofs making use of the reasoning called reductio ad absurdum are a little bit different ineffective proofs. Such a 'purely' existential proof consists in arguing the existence of some object or property on the ground of the supposition that its non-existence would lead to a contradiction. For example, Cantor was proving the existence of the transcendental numbers showing that an assumption about their non-existence led to a contradiction. Without such an assumption, the real numbers would consist of only algebraic numbers, or there would be only a few examples of transcendental numbers (Hermite proved in 1873 that e is indeed a transcendental number, and Lindemann proved in 1882 that the same was true for p ). It can't be so, however, because it is known that there exist countlessly many real numbers, whereas there are only countably many algebraic numbers. In this case, the assumption of the non-existence of transcendental numbers leads to the conclusion that, on the one hand, there is an uncountable number of real numbers, while on the other hand, there is only a countable number of them: thus we are led to a contradiction, so we must assume that the assumption (about the non-existence of transcendental numbers) is false.

The situation connected with the occurrence of the existential proofs was perceived by at least some mathematicians as unsatisfactory. If we add to that the discovery of the famous antinomies in the set theory, and the indication, by Poincaré and Klein, that non-Euclidean geometries, from the formal point of view, are not "worse" than Euclidean geometry, then we will achieve the picture which led to the collapse of the faith not only in the traditional mathematical proof, but also in the obviousness and consistency of the whole mathematics. The way out from this hitherto existing situation, which was proposed at the end of the XIX century, was another "revolution of precision".

Mathematics based on the intuitive clarity and self-obviousness, after these pillars were shaken, is forced to support itself by other methods. It can, for example, impose higher requirements as to the formal-logical side of its reasoning, in order to be more independent from subjective factors. The rapid development of mathematical knowledge delivered the tools for the realization of this programme. A widespread application of the results of mathematical logic in mathematics led to the formalization of notions, axioms and rules of demonstration, and through that, to the emergence of the formalized mathematical theories. They appeared within the framework of the so-called Hilbert's Program, the program of constructing an 'absolute' proof of the consistency of mathematics. Hilbert was convinced that every mathematical theory could be presented as a system of formulas linked together by a finite number of structural relations, whose research can show that no contradictory sentences can be derived from the axioms of the theory. To achieve this purpose in a formal way, we have to clearly define first of all the language of the system we are going to use, and in it the set of sensible expressions together with the sub-set of axioms, and assume that the initial symbols do not have semantic meaning (or that we must abstract from the primitive meaning of given symbols). The proofs in so defined a system, called formalized proofs, should be conducted only on the basis of precisely defined rules of transformation of expressions, referring not to their content but to their form. In other words, they are treated simply as a sequence of distinguishable symbols, for example signs on paper, which are subject to specific restrictions of formation and transformation.

Characterising the formalized proof in a different way, we could say that it is a finite succession of 'mechanical' transformations conducted on the physical elements (graphic signs). These elements are devoid of any semantic characteristic, apart from being combinations of symbols, distinguishable from each other. A necessary property of formalized proofs is their finitism and a lack of reference to obviousness and intuitiveness. Each demonstration step is an application of some explicitly mentioned interference rule, and this is the difference with semi-formal proofs, in which the very demonstration reasoning was, at the contrary, of "intuitive" nature. A mathematical proof in this form loses some of its comprehensibility because it appeals neither to content nor to intuition but only to the form of expressions. The question about the adequacy of the proof can be asked only in the framework of some methodological conception of a theory or of a proof, by assuming a definite logical system. On the ground of this system, what can be proved, can be proved absolutely precisely as far as the formal aspect is concerned, where all the methodological rules defining the rules of creating proofs are explicitly formulated.

This doesn't imply that formalized proofs can't undergo criticism. When all the requirements regarding the demonstration procedure are fulfilled, the convictions which lie at the foundations of the conception of formal systems and, more widely, of the whole formalization process, can become object of criticism. Unquestionably, the formalization method translates content mathematics to the form in which it is easier to analyse it. It seems, however, that they are not simply the equivalents of the theory of classical mathematics, but the deformed, 'wrung out pictures' of these theories, in which, on the one hand, the given theories are presented in a precise form but, on the other hand, they always contain 'a little bit too much' or 'a little bit too little', thus remaining inadequate towards the prototype. Contrary to appearances, the formalization process isn't neutral to the formalized theory, it unnoticeably subtracts some of the properties of the objects, previously comprehended intuitively or it adds unexpectedly new properties to the seemingly well-known objects or notions. Mathematicians know very well what intuitions are hidden behind such notions as: continuity, continuous function, dimension. After formalization of these notions, i.e. after defining them precisely and presenting them symbolically, it appeared that they gained some properties, totally extraneous to their primitive intuition. The examples of such a type of inadequacy are: a continuous function which is nowhere differentiable (everywhere 'hispid'), surfaces which only admit the zero field, curves of fractional dimensions or totally filling the surface of a square, etc..

Therefore it should be checked whether the formal theorems with their formal proofs can be good representatives of their classical contents equivalents. This problem was raised by Tarski, who was convinced that in order to properly evaluate the notion of formal proof, we have to explain its relation to the notion of truth. It is something like coming back to the problem connected with the primary task which had to be fulfilled by a proof, i.e. the task of convincing about the truth of some mathematical assertions. Tarski asks the question if the formal proof is really an adequate method of reaching the truth. With the help of reasoning conducted in metalanguage, patterned on the method of the proof of the famous Gödel's theorem, Tarski shows that the set of the provable sentences of a given formalized theory is not identical with the set of the true sentences of the theory. There exist sentences formulated in the language of a given theory, which are true but cannot be proved, in other words, the notion of demonstrability cannot fully substitute the notion of truth in the domain of mathematics. In connection with that, we have to take into account the possibility that in every, a little bit richer mathematical theory (i.e., which contains at least the formal system of arithmetic), there exist some interesting and non-trivial theorems which we won't be able to prove in any formal way. This is really what Gö del¹¹ showed in his famous incompleteness theorem. This fact can be interpreted as a process of running out the heuristic possibilities of a deductive demonstration method in mathematics.

Even if it was so, then the existence of the limits of applicability of some research method doesn't disqualify it automatically. Sometimes the awareness of the limitations of the applied research tools is treated as a higher stage of methodological knowledge, positively influencing the whole research, since we know what we can and what we can't achieve using this method. I think that we should treat the limitations connected with the formalized proofs in this way. If we restrict ourselves to the theorems which are deductive consequences of some number of axioms, accepted in our mathematical theory, then in force of Gö del's theorem we have no chance to reach epistemologically some theorems which lie outside the limits of the formal method.

However such a conclusion in the light of new facts is not unavoidable. Here I mean the more and more clearly emerging possibility of applying computers in order to achieve qualitatively new mathematical results. The contemporary computer technology is so advanced that we can hope that the presently constructed computers will satisfy the requirements of a theoretical abstract reasoning. I leave open this problem, because the question concerning the influence of the application of computers in mathematics exceeds the limits of the present article.
 

1. The common pseudonym of a big group of contemporary mathematicians, mainly French.

2. I am citing after Zeeman, E. C., Research, Ancient and Modern, in: Bulletin of the Institute of Mathematics and Its Applications 10, 1974.

3. It is a controversial thesis as there arises the problem of the so-called Babylonian or Egyptian mathematics. In accordance with the conception of mathematics presented in this paper, the achievements concerning calculations or measurements of the pre-Greek cultures cannot be called mathematics but rather the exhibition of practical mathematical skills. Under the influence of philosophy, in this empirical mathematics there occurred an epistemological cut, whose consequence was that mathematics became theoretically oriented.

4. See Newson, C. V., Mathematical Discourses. The Heart of Mathematical Science, Prentice - Hall, Inc., Englewood Cliffs, N. J. 1964.

5. See Tarski, A., Truth and proof, in: Scientific American 6, 1969.

6. See Davis, P. J. & Hersh, R. The mathematical Experience, Birkhä user Boston, 1981.

7. See Garding, L. Encounter with Mathematics, Springer - Verlag New York Inc, 1977.

8. This theorem is analysed in detail by Imre Lakatos: Proofs and Refutations. The Logic of Mathematical Discovery, Cambridge University Press, 1976.

9. From the formalistic point of view.

10. It is the problem of general assumptions concerning the accepted logic, the rules of interference, and so on.

11. See Nagel, K. & Newman, J. R., Gö del's Proof, New York University Press, 1959.
 

[A presentation of the author can be found in Episteme N. 6, Part II]

Department for Logic, Methodology and Philosophy of Science
University of Gdansk, ul. Bielanska 5 - 80-952 Gdansk, Poland

filjam@univ.gda.pl