Читать книгу Lógos and Máthma 2 - Roman Murawski - Страница 20

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 theorem eventually comes to be viewed as an obvious corollary of a larger theoretical construct. Thus proofs are a means for establishing what is real and what is not, but also a vehicle for arriving at a deeper understanding of mathematical reality.

There are many examples from the history of mathematics that confirm this. In this context, one can mention Paul Erdős’ idea of proofs from The Book in which God maintains the perfect proofs for mathematical theorems – he followed the dictum of G.H.Hardy that there is no permanent place for ugly mathematics. Erdős stressed that one need not believe in God but, as a mathematician, one should believe in The Book.23

Note that a proof that convinces can be more (or even quite) formal. Explanatory proofs cannot be strictly formal. Mathematicians set a high value on explanatory proofs. Such a proof is more valued when “it exhibits methods that are powerful and informative” (Avigad 2006, p. 106).Hersh says in (1997, p. 60) that “[p]roof is a tool in service of research, not a shackle on the mathematician’s imagination”.24

Sometimes theorems are verified in mathematics by checking all particular cases, but this usually does not give an explanation why the theorem holds. The explanation should give a general principle by which the theorem holds. a famous example of a theorem verified by checking cases but not giving reasons is the Four-Color Theorem proved by Appel and Haken and stating that every planar graph is four-colourable, i.e. in another words, that four colours suffice to colour everymap ←42 | 43→on the plane in such a way that two regions receive different colours whenever they have a common border.

The example of the Four-Color Theorem indicates other features of proofs in mathematics. Observe that the first purported proof of it given by Kempe in 1879 was accepted for a decade before it was found to be incorrect. This was neither the first nor the last example of such a situation. It means that the community of mathematicians can be fallible.

The Four-Color Theorem opened eyes of philosophers of mathematics to the problem of methods acceptable in a proof or in a verification of cases. The unique known proof – that by Appel and Haken – was obtained by using computer, and no traditional proof (without computer) is known so far. Moreover, the existing proof cannot be made by a human being because an essential part of it was a computation requiring about 1200 hours of computer time and is beyond the capacities of any mathematician. This initiated a discussion concerning the admissibility of experimental methods in mathematical proofs. Several arguments pro and contra have been formulated – we will not enter here the details of the discussion. Let us say only that the usage of a technical tool (like a computer) seems to refute the commonly accepted thesis that mathematical knowledge is a priori. There arises also a question whether a computer-aided proof is (or can be treated as) a mathematical proof and consequently, whether in particular the Four-Color Theorem can be called “theorem” or it is still rather a hypothesis.

In this debate initiated by a paper by Tymoczko (1979) a question was asked what are in fact the characteristic features of a “normal”mathematical proof. Tymoczko says that a proof in mathematics should be: (1) convincing, (2) surveyable and (3) formalizable.

The first feature is – as Tymoczko says – of an “anthropological” character, the other two are treated by him as “deep features”. He claims also that “surveyability and formalizability can be seen as two sides of the same coin” (Tymoczko 1979, p. 61). Formalizability “idealizes surveyability, analyzes it into finite reiterations of surveyable patters” (ibidem). It can be assumed that all surveyable proofs are formalizable. Are also all formalizable proofs surveyable? Tymoczko answers this negatively: “[w]e know that there must exist formal proofs that cannot be surveyed by mathematicians if only because the proofs are too long or involve formulas that are too long” and the phrase “too long” means here “can’t be read over by a mathematician in a human life time” (ibidem). On the other hand, one should observe that “it is not at all obvious that mathematicians could come across formal proofs and recognize them as such without being able to survey them” (Tymoczko 1979, p. 62).

Considering surveyability one should distinguish local and global surveyability. Bassler in (2006, p. 100) characterizes them in the following way:

←43 | 44→

local surveyability requires the surveying of each of the individual steps in a proof in some order, while global surveyability requires the surveying of the entire proof as a comprehensive whole.

Hence, a local surveyability does not mean that a proof is practically surveyable. One can say that the proof of the Four-Color Theorem is globally surveyable without being locally surveyable (provided one is willing to countenance a distinction between proof and calculation). On the other hand, if one accepts the assumption that global surveyability receives its foundation in local surveyability then this statement is false. Add that one should also distinguish the surveyability of a proof and the fact that it can be (formally) checked on the one hand and the fact that it gives an understanding, that it reveals the deep reasons for the theorem being proved on the other.

The concept of surveyability is not precise enough. In the 20th century, there was a trend to link surveyability with the development of formal and complete foundations of mathematics, and formalization was treated as a method providing the local surveyability. The works of Frege, Russell and their followers, especially Hilbert, were guided by the desire to find a perspicuous syntactic representation of the relations of semantic content within a proposition.

Computers and methods connected with them were and are used in mathematics not only in the proof of the Four-Color Theorem. They are used in various contexts in mathematics, in particular: (1) to perform numerical calculations, (2) to find (usually approximate) solutions of equations and systems of algebraic or differential equations or of integrals, (3) in automating proofs of theorems, (4) in checking the correctness of mathematical proofs, (5) in proving theorems (one says then about computer-aided proofs) and (6) in various experiments with mathematical objects (e.g., in the theory of fractals).

From our point of view, the most important applications are (3) and (4) – the application of the type (5) has been discussed above on the example of the Four-Color Theorem.

The automating proving of theorems is connected with the idea of mechanization and automatization of reasoning due to Leibniz (cf. Marciszewski and Murawski 1995). This idea (as one of the factors) led to the development of formal logic and in consequence to the idea of a formal proof.