Lógos and Máthma 2. Roman Murawski

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.

      Formal proofs and their role

      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