Fachwerk oder Schema von Begriffen nebst ihren nothwendigen Beziehungen zu einander, und die Grundelemente können in beliebiger Weise gedacht werden. Wenn ich unter meinen Punkten irgendwelche Systeme von Dingen, z.B. das System: Liebe, Gesetz, Schornsteinfeger [...] denke und dann nur meine sämtlichen Axiome als Beziehungen zwischen diesen Dingen annehme, so gelten meine Sätze, z.B. der Pythagoras auch von diesen Dingen.Mit anderen Worten: eine jede Theorie kann stets auf unendliche viele Systeme von Grundelementen angewandt werden”.
16 Cf. Gödel’s letter to Hao Wang dated 7th December 1967 – see Wang (1974), p. 8.
17 For the problem of the priority of proving the undefinability of truth, see Woleński (1991) and Murawski (1998).
18 Construction of SatΣn and SatΠn can be found in Kaye (1991) and Murawski (1999).
19 Note that many of those theorems hold not only for Peano arithmetic PA but also for a broad class of theories – cf.Niebergall (1996).
20 One should distinguish the truth in mathematics and the truth of mathematics.
21 Note that, as indicated above, Hilbert was not interested in philosophical questions and did not consider them.
←36 | 37→
Some Historical, Philosophical and Methodological Remarks on Proof in Mathematics
Introduction
Proofs play an important role in mathematics and its methodology (in the context of justification).They form the main method of justifying mathematical statements. Only statements that have been proved can be treated as belonging to the corpus of mathematical knowledge. Proofs are used to convince the readers of the truth of presented theorems. But what is in fact a proof? In mathematical research practice, proof is a sequence of arguments that should show the truth of the claim. Of course, the particular arguments used in a proof depend on the situation, on the audience, on the type of a claim, etc. Hence a concept of a proof has in fact a cultural, psychological and historical character. In practice, mathematicians generally agree whether a given argumentation is or is not a proof. More difficult is the task to define a proof as such. Beside proofs used in the research practice there is a concept of a formal proof developed by logic. What are the relations between them? What roles do they play in mathematics?
Problems of that type will be considered in the paper. We start by some historical remarks showing in what circumstance the idea of a proof (informal and formal) appeared. Next, the features and role played by informal proofs will be considered. The subject of the next section will be formal proofs and their relation to the concept of truth. In the closing section, some conclusions will be made and a thesis (similar to Church-Turing Thesis in the computation theory) formulated.
Historical remarks
The model of mathematics as a science, its paradigm functioning in fact till today, was formulated and developed in the ancient Greece about 4th century B.C. Earlier, e.g. in ancient Egypt or Babylon, mathematics consisted of practical procedures that should help to solve everyday problems such as measuring surface area or the amount of cereal in a granary or oil in a jug. In those both pre- Greek mathematics – though they were advanced and sophisticated (especially the Babylonian mathematics) – there was no need to prove statements. In fact, there were no general statements and no attempts were undertaken to deduce the results or to explain their validity. One was satisfied by instructions what should be done in order to receive the result or to perform the required task. In fact, mathematics there was a collection of separate algorithms (as one would say today) and resembled ←37 | 38→in certain sense informatics (though without sophisticated technical equipment). Similar was the situation in China – Chinese mathematics was also a collection of procedures (transferred from generation to generation).
Proofs as deduction from explicitly stated postulates was conceived by the Greeks. It was connected with the axiomatic method. Since Plato, Aristotle and Euclid the axiomatic method was considered as the best method to justify and to organize mathematical knowledge. The first mature and most representative example of its usage in mathematics was the Elements of Euclid. They established a pattern of a scientific theory and in particular 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, postulates and definitions. Axioms were principles common to all sciences, postulates – specific principles taken for granted by a mathematician engaged in the demonstration of theorems in a particular domain. Definitions should provide meaning to new notions – in practice definitions were rather explanations of notions than proper definitions in the strict sense, moreover, they were explanations in the unprecise everyday colloquial language. Note that the language of a theory was not separated from the natural language. 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. Consequently, proofs were only partially based on axioms and postulates. In fact proofs were informal and intuitive, they were rather demonstrations and the very concept of a proof was of a psychological and sociological (and not of a logical) nature.
Note that the language of theories was simply the unprecise colloquial language. Till the end of the 19th century, mathematicians were convinced that axioms and postulates should be true statements, hence sentences describing the real state of affairs (in the mathematical reality).22 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.
It should be noted that Euclid’s approach (connected with Platonic idealism) to the problem of the development of mathematics and the justification of its statements (which found its fulfilment in the Euclidean paradigm), i.e. justification by deduction (by proofs) from explicitly stated axioms and postulates, was not the only approach and method which was used in the ancient Greek (and later). The ←38 | 39→other one (call it heuristic) was connected with Democritus’ materialism. It was applied, e.g., by Archimedes who used in his mathematical works not only deduction but any methods, such as intuition or even experiments (not only mental ones) to solve problems. One can see this, e.g., in his considerations concerning the calculation of the volume of a sphere using cylinder with two excavated cones or in his quadrature of the parable.
Though the Euclidean approach won and dominated in the history, one should note that it formed rather an ideal and not the real scientific practice of mathematicians. In fact rigorous, deductive mathematics was rather a rare phenomenon. On the contrary, intuition and heuristic reasoning were the animating forces of mathematical research practice. The vigorous but rarely rigorous mathematical activity produced “crises” (e.g. the Pythagoreans’ discovery of the incommensurability of the diagonal and the side of a square, Leibniz’s and Newton’s problems with the explanation of the nature of infinitesimals, Fourier’s “proof ” that any function is representable in a Fourier series, antinomies connected with Cantor’s imprecise and intuitive notion of a set).
New elements appeared in the 19th century with the trend whose aim was the clarification
