(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
