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.
←52 | 53→
The Status of Church’s Thesis
Co-authored by Jan Woleński
The Church’s Thesis can be simply stated as the following equivalence: (CT) A function is effectively computable if and only if it is partially recursive.30
Thus (CT) identifies the class of effectively computable or calculable (we will treat these two categories as equivalent) functions with the class of partially recursive functions. This means that every element belonging to the former class is also a member of the latter class and reversely. Clearly, (CT) generates an extensional co-extensiveness of effective computability and partial recursivity. Since we have no mathematical tasks, the exact definition of recursive functions and their properties is not relevant here. On the other hand, we want to stress the property of being effective computable, which plays a basic role in philosophical thinking about (CT).31
A useful notion in providing intuitions concerning effectiveness is that of an algorithm. It refers to a completely specified procedure for solving problems of a given type. Important here is that an algorithm does not require creativity, ingenuity or intuition (only the ability to recognize symbols is assumed) and that its application is prescribed in advance and does not depend upon any empirical or random factors. Moreover, this procedure is performable in a finite number of steps. Thus a function f ∶ Nn → N is said to be effectively computable (briefly: computable) if and only if its values can be computed by an algorithm. Putting this in other words: a function f ∶Nn →N is computable if and only if there exists a mechanical method by which for any n-tuple (a1, . . . , an) of arguments, the value f (a1, . . . , an) can be calculated in a finite number of prescribed steps. Three facts should be stressed here: (a) no actual human computability or empirically feasible computability is assumed in (CT); (b) functions are treated extensionally, ←53 | 54→i.e. a function is identified with an appropriate set of ordered pairs; (c) the concept of computability has a modal parameter (“there exists a method”, “a method is possible”) as its inherent feature.
Typical comments about (CT) are as follows:
(i) Church’s thesis is not a mathematical theorem which can be proved or disproved in the exact mathematical sense, for it states the identity of two notions only one of which is mathematically defined while the other is used by mathematicians without exact definition.32 (Kalmár 1959, p. 72)
(ii)While we cannot prove Church’s thesis, since its role is to delimit precisely a hitherto vaguely conceived totality, we require evidence that it cannot conflict with the intuitive notion which is supposed to be complete; i.e. we require evidence that every particular function which our intuitive notion would authenticate as effectively calculable is [...] recursive. The thesis may be considered a hypothesis about the intuitive notion of effective calculability; in the latter case, the evidence is required to give the theory based on the definition the intended significance. (Kleene 1952, pp. 318–319), Kleene 1967, p. 232)
(iii) This is a thesis rather than a theorem, in as much as it proposes to identify a somewhat intuitive concept phrased in exact mathematical terms, and thus is not susceptible of proof. But very strong evidence was adduced by Church, and subsequently by others, in support of the thesis.
It [(CT) – and other similar characterizations – our remark, R.M. and J.W.] must be accepted or rejected on grounds that are, in large part, empirical. [...]. Church’s Thesis may be viewed as a proposal as well as a claim, that we agree henceforth