It was undoubtedly a great achievement of modern logic to have replaced the old psychological notion of proof, which could hardly ever be made clear and precise, by a new simple notion of a purely formal character. But the triumph of the method carried with it the germ of a future setback.
Considerations concerning formal proofs enlightened also the role played by infinity in mathematics, in particular in the process of proving.Gödel’s results show that finite/finitistic methods of syntactical formal provability do not exhaust the variety of mathematical truth. In fact, if one wants to obtain a complete theory then some infinite/infinitistic rules (such as the ω-rule) are necessary. Recall that the ω-rule is an inference rule with infinitely many premisses, i.e. it is the following rule:
In mathematical research practice, nobody restricts himself/herself to finite methods; on the contrary, any correct methods, among them infinite (in particular set-theoretical and semantical), are applied. Being not so ideal as it was hoped, formal proofs play an important role in metamathematics, i.e. in the study of mathematical theories or of mathematics as a collection of theories – but not only there. ←47 | 48→They enable also the automatization and mechanization of proofs in mathematics, hence they make possible the construction of automated proofs and the verification of proofs by computers. Verification of (formal) proofs is possible because the relation “x is a proof of y” is – as was shown in mathematical logic – recursive, hence effective and can be implemented. On the other hand, constructing and finding proofs is not an effective (recursive) procedure; there is no universal method of doing this (as results of Turing, Church and Gödel show). In fact, it is only recursively enumerable. Hence every formal proof is a result of a creative invention of a human being. One can say that “[f]ormalization is about checking, and not about discovery” (cf.Wiedijk 2008, p. 1414).
Observe that the concept of a formalized proof is one for all theories; it is in a sense a uniform concept. It is independent of subjective, cultural and sociological elements and factors. Moreover, the completeness theorem of Gödel states that the logical means of the first-order logic (first-order predicate calculus) are sufficient.27 This concept enables us to make the concept of a proof more objective. It also makes possible the precise study of provability in mathematics – under the assumption that the logical concept of a proof reflects all important and essential features of proofs from the research practice of mathematicians. One can prove results stating that a given statement is not a theorem of a given theory, i.e. that there exist no (formal) proof of a given statement or that a given sentence is (formally) undecidable (in a given theory). It enables also the study of important metamathematical properties of mathematical theories such as consistency, completeness, independence of axioms or axiomatizability in a given way, etc.
The concept of a formal proof is also helpful in the philosophy of mathematics. It can be used in attempts to answer the question about the existence and character of mathematical objects as well as in considerations concerning the epistemology of mathematics. On the other hand, all philosophies of mathematics reducing mathematics to formalized axiomatic theories (among them logicism and formalism) have a reductionist character and do not take into account the actual research practice of mathematicians. Their aim is to justify mathematics and not to explain the real mathematical practice. It is worth noting that in recent trends in the philosophy of mathematics still more and more attention is paid to the study of the research practice in mathematics – one takes into account various sociological, psychological and cultural factors. Unfortunately, it is done only by the analysis of particular single discoveries and achievements, hence by case studies. There are no general conceptions. But is it possible to develop such general conceptions?
←48 | 49→
In fact, formal proofs are connected rather with foundational studies than with research practice. Observe that a formal proof does not give an understanding; it does not explain the deep reasons of a theorem. They are also not suitable for the practice – they are simply too long, they are too tedious and painstaking. In such a proof, the underlying intuition may get lost. Formalized mathematics may be also more error-prone than the usual informal one – in fact, formal manipulationsmay become very complicated. As Bourbaki (1968) wrote:
If formalized mathematics were as simple as the game of chess, then once our chosen formalized language had been described there would remain only the task of writing out proofs in this langauge, [...]. But the matter is far from being as simple as that, and no great experience is necessary to perceive that such a project is absolutely unrealizable: the tinest proof at the beginning of the Theory of Sets would already require several hundreds of signs for its complete formalization. [...] formalized mathematics cannot in practice be written down in full, [...].We shall therefore very quickly abandon formalized mathematics, [...].
Cadwallader Olsker (2011, p. 42) writes:
a purely formal proof [...] cannot be very complex without becoming so lengthy as to be incomprehensible to a human reader. Such a formal proof is rarely able to be explanatory, and may only be convincing to the degree that it can be read and understood by the reader or checked by a computer.
Add that a transcription of a single traditional (hence informal) proof into a formal one is a major undertaking.
Conclusion
We have shown that one has two concepts of a proof in mathematics: an informal one used by mathematicians in their usual research practice and the concept of a formal or formalized proof used mainly in logic and the foundations of mathematics. The first one is not defined precisely; it is simply practised and any attempts to define it fail. It is – so to speak – a practical notion. It has a psychological, sociological and cultural character. The second one is precisely defined in terms of logical concepts. Hence, it is a logical concept having rather theoretical than practical character. The first one has – in a part at least – semantical character, and the second is entirely syntactical in nature.
Hence this situation can be compared with the situation concerning Church-Turing thesis. This thesis states the equivalence of two concepts: effective computability (in the intuitive sense) and recursiveness (or Turing computability or computability in the sense of Markov or any other precisely defined and equivalent sense). As is known, this equivalence cannot be proved with the degree of precision usual and required in mathematics. The reason is that one part of this ←49 | 50→equivalence contains an intuitive vague concept formulated in the everyday language and the other a precise concept defined in the language of mathematics (cf. Murawski 2004b as well as Murawski and Wolenski 2006).
With such a situation, one has to do also in other parts of mathematics – see, for example, the concepts of function, of truth, of logical validity or of limit (cf. Mendelson 1990). In fact, till the 19th century a function was tied to a rule for calculating it, generally by means of a formula. In 19th and 20th centuries mathematicians started to define a function as a set of ordered pairs satisfying appropriate conditions (hence a function is identified here with its graph). The identification of those notions, i.e., of an intuitive notion and the precise set-theoretical one, can be called “Peano thesis”. Similarly, “Tarki’s thesis” is the thesis identifying the intuitive notion of truth and the precise notion of truth given by Tarski in (1933).The intuitive notion of a limit widely used in mathematical analysis in the 18th century and then in the 19th century applied by A. Cauchy to define basic notions of the calculus has been given a precise form only by K. Weierstrass in the language of “ε−δ”. There are many other such examples: the notion of a measure as an explication of area and volume, the definition of dimension in topology, the definition of velocity as a derivative, etc.
Comparing the two