**(Jaroslaw Mrozek)**

**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^{1} - 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".^{2}
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.^{3} 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.^{4}

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.^{5} 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^{6},
or the theorem about the *existence of infinitely many prime numbers*,
formulated and proved by Euclid in his famous *Elements*.^{7}
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 _{1} and B_{1} so that the proportion
AA_{1} :BB_{1} 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.^{8}

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^{9}, 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.^{10} 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 ^{n} , and T : B^{n} ®
B^{n} is a continuous mapping, then there exists a point x_{0}
Î B^{n} such that T(x_{0})
= x_{0}*.

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 _{1},x_{2} > , and the values
of the function at the end points of the interval: f(x_{1}), f(x_{2})
have different signs, i.e [f(x_{1})*
f(x_{2})] < 0, then there exists
a point*

**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^{11} 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.

**Notes**

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