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

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 concepts of a proof in mathematics one can formulate a thesis stating that they are equivalent – one can call such a thesis a proof-theoretical thesis.28 As in the case of Church Thesis, no precise and strict proof of it can be given.29 One can only formulate arguments in favour or against it. The main argument for this thesis is the conviction – being popular among mathematicians and logicians – that every “normal” mathematical proof can be formalized, i.e. can be written as a formal proof in a suitable axiomatic theory. There are, of course, no general rules describing how this can and should be done. In fact, a formalization of an informal proof requires often some original and not so obvious ideas.

In this way, we come to the following conclusion: there are two concepts of a proof in mathematics. They play different but complementary roles: formal proofs ←50 | 51→are used mainly in metamathematical and logical considerations, whereas informal proofs are used in the research practice of mathematicians.

Note. The paper is based on my talks at the conferences Philosophy in Science (Kraków, Poland, 2012) and Proof (International Conference within the frame of Humboldt-Kollegs, Bern, Switzerland, 2013). I would like to thank the referee for helpful comments and suggestions.

←51 | 52→

22 In fact, the discussion about the truth of mathematical statements started already with the discovery of non-Euclidean geometries, but the conviction of the truth of mathematical theses dominated.

23 In 1998, Springer Verlag published Proofs From The Book by M. Aigner and G.M. Ziegler (cf. Aigner and Ziegler 1998). It is treated by the authors as “a first (and very modest) approximation of The Book” (Preface).

24 On the concept of explanation in mathematics see, e.g. Steiner (1978) and Mancosu (2000, 2001).

25 Note that there was at that time no precise definition of truth – this was given only in 1933 by A. Tarski (1933).

26 Cf. Gödel’s letter to Hao Wang dated 7th December 1967 – see Wang (1974, p. 9). He wrote there: “I may add that my objectivist conception of mathematics and metamathematics in general, and of transfinite reasoning in particular, was fundamental also to my other work in logic. How indeed could one think of expressing metamathematics in the mathematical systems themselves, if the latter are considered to consist of meaningless symbols which acquire some substitute of meaning only through metamathematics. [...] it should be noted that the heuristic principle of my construction of undecidable number theoretical propositions in the formal systems of mathematics is the highly transfinite concept of ‘objectivemathematical truth’ as opposed to that of ‘demonstrability’ (cf. M. Davis, The Undecidable, New York 1965, p. 64, where I explain the heuristic argument by which I arrive at the incompleteness results), with which it was generally confused before my own and Tarski’s work”.

27 Note that in the case of, e. g., second-order logic the situation is different – one does not have here the completeness phenomenon.

28 Add that this formulation is consciously rather vague – e.g. it is not specified here in which formal theory (or theories) formal proofs should be constructed and what should be the underlying logic. A similar but stronger thesis was formulated by Barwise (1977, p. 41) under the name “Hilbert’s Thesis” where he wrote: “... the informal notion of provable used in mathematics is made precise by the formal notion provable in first-order logic. Following the sug[g]estion of Martin Davis, we refer to this view as Hilbert’s Thesis”. This thesis says that first-order logic is the logic of mathematics.

29 Note that in the case of Church Thesis the formal framework is precisely specified: the intuitive notion of computability should be captured by one specific formal model of computation.