4 Both those aspects are interconnected – as was indicated by G. Kreisel. He showed that if φ is a
5 Hilbert rejected the opinion that Gödel’s results showed the non-executability of his programme. He claimed that they have shown “only that for more advanced consistency proofs one must use the finitistic standpoint in a deeper way than is necessary for the consideration of elementary formalisms” (cf. Hilbert and Bernays 1934–1939, vol. I). Gödel wrote in (1931) that “Theorem XI [i.e. Gödel’s second theorem for arithmetic P where P denotes the arithmetic of Peano extended by simple type theory – my remark, R.M.] (and the corresponding results for M and A) [where M is the set theory and A is the analysis – my remark, R.M.] do not contradict Hilbert’s formalistic viewpoint. For this viewpoint presupposes only the existence of a consistency proof in which nothing but finitary means of proof is used, and it is conceivable that there exist finitary proofs that cannot be expressed in the formalism of P (or Mor A)”.
6 It seems that Bernays was among the first who recognized this need. He wrote: “It thus became apparent that the ‘finite Standpunkt’ is not the only alternative to classical ways of reasoning and is not necessary implied by the idea of proof theory. An enlarging of the methods of proof theory was therefore suggested: instead of a restriction to finitist methods of reasoning, it was required only that the arguments be of a constructive character, allowing us to deal with more general forms of inference” (cf. Bernays 1967, p. 502).
7 For the description of PRA see, e.g. Smoryński (1977).
8 This was first observed by Hilbert and Bernays. Weyl (1918) had shown that a substantial part of ordinary mathematics can be developed within a certain “predicative” subsystem of Z2 (allowing ω-iterated arithmetical definability).
9 Recall that H. Poincaré saw the source of antinomies in mathematics just in impredicativity and therefore demanded a restriction to predicative methods only.
10 Drake claims even that the implications of the results of reverse mathematics “make much of what was written in the past on the philosophy of mathematics, obsolete” (cf. Drake 1989).
11 For the definition of and basic information on the arithmetical and analytical hierarchies of formulas and relations see, e.g. Shoenfield (1967).
12 Denote by WO(α) the sentence stating that the ordinal α is a well-ordered set. One can prove in RCA0 that WO(ωω) is equivalent to Hilbert’s basis theorem. But the sentence WO (ωω) is incomparable with WKL0.On the other hand, for any given natural number n one can prove in RCA0 that WO(ωn) is equivalent to Hilbert’s basis theorem for n. What more, WO(ωn) is provable in RCA0. So we have here certain analogy with the ω–incompleteness of Peano arithmetic (cf. Gödel 1931, see also Mendelson 1970).
13 Hilbert asked in his 17th problem “whether every definite form [of any number of variables with real coefficients – my remark, R.M.] may not be expressed as a quotient of sums of squares of forms” (cf. Hilbert 1901, see also Browder 1976). Recall that a form is called “definite” if it becomes negative for no real values of the variables. In 1926, Artin answered this question positively.
←22 | 23→
On the Distinction Proof–Truth in Mathematics
Concepts of proof and truth are (even in mathematics) ambiguous. It is commonly accepted that proof is the ultimate warrant for a mathematical proposition, that proof is a source of truth in mathematics. One can say that a proposition A is true if it holds in a considered structure or if we can prove it. But what is a proof? And what is truth?
The axiomatic method was considered (since Plato, Aristotle and Euclid) to be the best method to justify and to organize mathematical knowledge. The first mature and most representative example of its usage in mathematics were Elements of Euclid. They established a pattern of a scientific theory and a paradigm in mathematics. Since Euclid till the end of the 19th century, mathematics was developed as an axiomatic (in fact rather a quasi-axiomatic) theory based on axioms and postulates. Proofs of theorems contained several gaps – in fact the lists of axioms and postulates were not complete, one freely used in proofs various “obvious” truths or referred to the intuition. Proofs were informal and intuitive, they were rather demonstrations; and the very concept of a proof was of a psychological (and not of a logical) nature. Note that almost no attention was paid to the precization and specification of the language of theories – in fact the language of theories was simply the unprecise colloquial language. One should also note here that in fact till the end of the 19th century, mathematicians were convinced that axioms and postulates should be true statements. It seems to be connected with Aristotle’s view that a proposition is demonstrated (proved to be true) by showing that it is a logical consequence of propositions already known to be true. Demonstration was conceived here of as a deduction whose premises are known to be true, and a deduction was conceived of as a chaining of immediate inferences.
Basic concepts underlying the Euclidean paradigm have been clarified on the turn of the 19th century. In particular, the intuitive (and rather psychological in nature) concept of an informal proof (demonstration) was replaced by a precise notion of a formal proof and of a consequence. This was the result of the development of mathematical logic and of a crisis of the foundations of mathematics on the turn of the 19th century which stimulated foundational investigations.
One of the directions of those foundational investigations was the program of David Hilbert and his Beweistheorie. Note at the very beginning that “this program was never intended as a comprehensive philosophy of mathematics; its purpose was instead to legitimate the entire corpus of mathematical knowledge” (cf. Rowe 1989, p. 200).Note also that Hilbert’s views were changing over the years, but always took a formalist direction.
←23 | 24→
Hilbert sought to justify mathematical theories by means of formal systems, i.e., using the axiomatic method. He viewed the latter as holding the key to a systematic organization of any sufficiently developed subject. In “Axiomatisches Denken” (1918, p. 405) Hilbert wrote:
When we put together the facts of a given more or less comprehensive field of our knowledge, then we notice soon that those facts can be ordered. This ordering is always introduced with the help of a certain network of concepts (Fachwerk von Begriffen) in such a way that to every object of the given field corresponds a concept of this network and to every fact within this field corresponds a logical relation between concepts. The network of concepts is nothing else than the theory of the field of knowledge.14
By Hilbert the formal frames were contentually motivated. First-order theories were viewed by him together with suitable non-empty