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

Formal proofs were introduced to provide an explication of the informal notion of a proof and to solve some metamathematical problems. They should explain the virtue by which usual proofs used in the research practice are judged to be correct. They should also explain what does it mean that a given statement is a logical or deductive consequence of certain assumptions. As indicated above they ←44 | 45→were introduced in the atmosphere of a crisis in the foundations of mathematics. For Frege and Russell they were means to an end, a way of precisely isolating the permissible proofs and making sure that all use of axioms was explicit. On the other hand, observe that Hilbert was not really interested in actually formalizing proofs and replacing the “normal” research proofs by formalized ones. He treated formalization and formal proofs as a tool to justify mathematics as a science and to establish its consistency. They should serve theoretical purposes – in particular to prove results about mathematics, hence to obtain metamathematical results.

In fact, the development of logic and the concept of a formal proof based only on syntactical properties made possible the development of metamathematics. A lot of interesting results have been obtained here. First of all the old paradigm of mathematics that was functioning since Euclid has been made precise – in fact it has been replaced by a new logico-set-theoretical paradigm (cf. Batóg 1996). The main features of this new paradigm can be described as follows: (1) Set theory became the fundamental domain of mathematics, in particular some set-theoretical notions and methods are present in any mathematical theory; and set theory is the basis of mathematics in the sense that all mathematical notions can be defined by primitive notions of set theory and all theorems of mathematics can be deduced from axioms of set theory. (2) Languages of mathematical theories are strictly separated from the natural language, they are artificial languages and the meaning of their terms is described exclusively by axioms; some primitive concepts are distinguished and all other notions are defined in terms of them according to precise rules of defining notions. (3) Mathematical theories have been axiomatized. (4) There is a precise and strict distinction between a mathematical theory and its language on the one hand and metatheory and its metalanguage on the other (the distinction was explicitly made by A. Tarski).

Note also that two concepts, crucial for mathematics: the concept of a syntactical consequence (being provable) and the concept of being a semantical consequence, have been precisely defined and strictly distinguished. One could also precisely distinguish provability and truth. In a “normal” research mathematical practice – as we indicated above – they are usually identified or at least not distinguished – one says that a theorem holds, i.e. has been proved (in a “normal”, informal sense of this notion), or that it is true and treats both as equivalent and synonymous. The very process of distinguishing them was long and not so simple – cf. Murawski (2002a, 2002b). The crucial role was played here by Gödel’s incompleteness theorems.

The incompleteness results of Gödel showed that any theory (based on a recursive set of axioms and finitary rules of inference) including arithmetic of natural numbers is in fact incomplete, hence there exist sentences that are true but are neither provable nor refutable, i.e. they are undecidable in a given theory. Before Gödel, it was believed that formal demonstrability is an analysis of the concept of ←45 | 46→mathematical truth. Gödel wrote in a letter of 7th March 1968 to Hao Wang (cf. Wang 1974, p. 10):

[...] formalists considered formal demonstrability to be an analysis of the concept of mathematical truth and, therefore were of course not in a position to distinguish the two.

Indeed, the informal concept of truth was not commonly accepted as a definite mathematical notion at that time.25 Gödel wrote in a crossed-out passage of a draft of his reply to a letter of the student Yossef Balas: “[...] a concept of objective mathematical truth as opposed to demonstrability was viewed with greatest suspicion and widely rejected as meaningless” (cf. Wang 1987, pp. 84–85). It is worth comparing this with a remark of R. Carnap. He writes in his diary that when he invited A. Tarski to speak on the concept of truth at the September 1935 International Congress for Scientific Philosophy, “Tarski was very sceptical. He thought that most philosophers, even those working in modern logic, would be not only indifferent, but hostile to the explication of the concept of truth”. And indeed at the Congress “[...] there was vehement opposition even on the side of our philosophical friends” (cf. Carnap 1963, pp. 61–62).

All these explains in some sense why Hilbert preferred to deal in his metamathematics solely with forms of formulas, using only finitary reasonings which were considered to be safe – contrary to semantical reasonings which were non-finitary and consequently not safe. Non-finitary reasonings in mathematics were considered to be meaningful only to the extent to which they could be interpreted or justified in terms of finitary metamathematics.26 On the other hand, there was no clear distinction between syntax and semantics at that time. Recall, for example, that the axiom systems came by Hilbert often with a built-in interpretation. Add also that the very notions necessary to formulate properly the difference syntax– semantics were not available to Hilbert though he was aware of the complex of ←46 | 47→problems – cf. his statement of the question in Hilbert and Ackermann (1928) which led to Gödel’s completeness theorem. Gödel proved that truth cannot be adequately achieved and expressed by provability, that the whole of mathematics (or even parts of it) cannot be included in a formalized system. This indicated certain weakness of the concept of a formal proof.Gödel’s results showed also that one should not limit or bound the creative invention of mathematicians. In the framework of formalized theories, one can extend them by adding new axioms or by admitting new inference rules. The second possibility means that infinitary rules are admitted – but this changes the whole picture and the whole paradigm! Note that Hilbert had in fact no problem with such a change, to the opposite – in view of Gödel’s result – he encouraged it. On the other hand, one can ask whether the process of adding new axioms, though necessary to solve problems undecidable in a given theory, is sufficient? Will it suffice to express the creativity of a mathematical mind, the creativity of mathematicians?

The incompleteness theorems of Gödel belong to the so-called limitation results. They are results stating that certain properties important and desired from a metamathematical point of view (but also from the point of view of a working mathematician) cannot be achieved. Among them is the theorem of Tarski stating the undefinability of the concept of truth and the theorem of Löwenheim and Skolem showing that a mathematical structure cannot be adequately and uniquely described by a formalized theory (a theory having a model has in fact many various models). Tarski wrote (1969, p. 74):

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.