From owner-qed Fri Nov 4 01:10:58 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id BAA23463 for qed-out; Fri, 4 Nov 1994 01:10:20 -0600 Received: from lapsene.mii.lu.lv (root@lapsene.mii.lu.lv [159.148.60.2]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id BAA23458 for ; Fri, 4 Nov 1994 01:09:50 -0600 Received: from sisenis.mii.lu.lv by lapsene.mii.lu.lv with SMTP id AA14480 (5.67a8/IDA-1.4.4 for ); Fri, 4 Nov 1994 09:09:40 +0200 Received: by sisenis.mii.lu.lv id AA17731 (5.67a8/IDA-1.4.4 for QED discussions ); Fri, 4 Nov 1994 09:09:32 +0200 Date: Fri, 4 Nov 1994 09:09:30 +0200 (EET) From: Karlis Podnieks To: QED discussions Subject: Semantics Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-qed@mcs.anl.gov Precedence: bulk University of Latvia Institute of Mathematics and Computer Science K.Podnieks, Dr.Math. podnieks@mii.lu.lv PLATONISM, INTUITION AND THE NATURE OF MATHEMATICS Continued from #3 However, let us suppose that this is the case, and in 2094 somebody will prove a new theorem of the Calculus using a property of real numbers, never before used in mathematical reasoning. And then will all other mathematicians agree immediately that this property was "intended" already in 1994? At least, it will be impossible to verify this proposition: none of the mathematicians living today will survive 100 years. Presuming that intuitive mathematical concepts can possess some "hidden" properties which do not appear in practice for a long time we fall into the usual mathematical platonism (i.e. we assume that the "world" of mathematical objects exists independently of mathematical reasoning). Some of the intuitive concepts admit several different but, nevertheless, equivalent reconstructions. In this way an additional very important evidence of adequacy can be given. Thus, let us remember, again, various definitions of real numbers in terms of rational numbers. Cantor's definition was based upon convergent sequences of rational numbers. Dedekind defined real numbers as "cuts" in the set of rational numbers. One definition more could be obtained using (infinite) decimal fractions. The equivalence of all these definitions was proved (we cannot prove strongly the equivalence of the intuitive concept and its reconstruction, but we can prove - or disprove - the equivalence of two explicit reconstructions). Another striking example is the reconstruction of the intuitive notion of computability (the concept of algorithm). Since the 1930s several very different reconstructions of this notion were proposed: recursive functions, "Turing-machines" of A.M.Turing, lambda-calculus of A.Church, canonical systems of E.Post, normal algorithms of A.Markov, etc. And here, too, the equivalence of all these reconstructions was proved. The equivalence of different reconstructions of the same intuitive concept means that the volume of the reconstructed concepts is not accidental. This is a very important additional argument for replacing the intuitive concept by an explicit reconstruction. The trend to replace intuitive concepts by their more or less explicit reconstructions appears in the history of mathematics very definitely. Intuitive theories cannot develop without such reconstructions normally: the definiteness of the intuitive basic principles gets insufficient when the complexity of concepts and methods is growing. In most situations the reconstruction can be performed by the genetic method, but to reconstruct fundamental mathematical concepts the axiomatic method must be used (fundamental concepts are called fundamental just because they cannot be reduced to other concepts). Goedel's incompleteness theorem has provoked very much talking about insufficiency of the axiomatic method for a true reconstruction of the "alive, informal" mathematical thinking. Such people say that axiomatics are is not able to cover "all the treasures of the informal mathematics". All that is once again the usual mathematical platonism, converted into the methodological one (for a detailed analysis see Podnieks [1981, 1992]). Does the "axiomatic reasoning" differ in principle from the informal mathematical reasoning? Do there exist proofs in mathematics obtained not following the pattern "premises - conclusion"? If not, and every mathematical reasoning can be reduced to a chain of conclusions, we may ask: are these conclusions going on by some definite rules which do not change from one situation to another? And, if these rules are definite, can they being a function of the human brain be such that a complete explicit formulation is impossible? Today, if we cannot formulate some "rules" explicitly, then how can we demonstrate that they are definite? Therefore, it is nonsense to speak about the limited applicability of axiomatics: the limits of axiomatics coincide with the limits of mathematics itself! Goedel's incompleteness theorem is an argument against platonism, not against formalism! Goedel's theorem demonstrates that no fixed fantastic "world of ideas" can be perfect. Any fixed "world of ideas" leads us either to contradictions or to undecidable problems. In the process of evolution of mathematical theories axiomatization and intuition interact with each other. The axiomatization "clears up" the intuition when it has lost its way. But the axiomatization has also some unpleasant consequences: many steps of intuitive reasoning, expressed by a specialist very compactly, appear very long and tedious in an axiomatic theory. Therefore, after replacing intuitive theory by the axiomatic one (this replacement may be inequivalent because of defects in the intuitive theory) specialists learn a new intuition, and thus they restore the creative potency of their theory. Let us remember the history of axiomatization of set theory. In the 1890s contradictions were discovered in Cantor's intuitive set theory, they were removed by means of axiomatization. Of course, the axiomatic set theory of Zermelo-Fraenkel differs from Cantor's intuitive theory not only in its form, but also in some aspects of contents. For this reason specialists have developed new, modified intuitions (for example, the intuition of sets and proper classes), which allow them to work in the new theory successfully. Today, all serious theorems of set theory are proved intuitively, again. What are the main benefits of axiomatization? First, as we have seen, axiomatization allows to "correct" intuition: to remove inaccuracies, ambiguities and paradoxes which arise sometimes due to insufficient controllability of intuitive processes. Secondly, axiomatization allows to carry out a detailed analysis of relations between basic principles of a theory (to establish its dependence or independence, etc.), and between the principles and theorems (to prove some of theorems only a part of axioms is needed). Such investigations may lead to general theories which can be applied to several more specific theories (let us remember the theory of groups). Thirdly, sometimes after the axiomatization we can establish that the theory considered is not able to solve some of naturally arising problems (let us remember the continuum-problem in set theory). In such situations we may try to improve the theory, even developing several alternative theories. 4. Formal theories How far can we proceed in the axiomatization of some theory? Complete elimination of intuition, i.e. full reduction to a list of axioms and rules of inference. Is this possible? The work by G.Frege, B.Russell and D.Hilbert (the end of the XIXth - beginning of XXth century) showed how this can be done even with the most serious mathematical theories. All these theories were reduced to axioms and rules of inference without any admixture of intuition. Logical techniques developed by these men allow us today to axiomatize any theory based on a fixed system of principles (i.e. any mathematical theory). What do they look like - such pure axiomatic theories? They are called formal theories (formal systems or deductive systems) underlining that no step of reasoning can be done in them without a reference to an exactly formulated list of axioms and rules of inference. Even the most "self-evident" logical principles (like, "if A implies B, and B implies C, then A implies C") must be either formulated in the list of axioms and rules explicitly or derived from it. The exact definition of the "formal" can be given in terms of the theory of algorithms (i.e. recursive functions): a theory T is called formal, if an algorithm (i.e. mechanically applicable computation procedure) is presented for checking correctness of reasoning via principles of T. It means that when somebody is going to publish a "mathematical text" calling it "a proof of a theorem in T", we can check mechanically whether the text in question really is a proof according to standards of reasoning accepted in T. Thus, the standards of reasoning in T are defined precisely enough to enable the checking of proofs by means of a computer program (note that we discuss here checking of ready proofs, not the problem of provability!). As an unpractical example of formal theory let us consider the game of chess, let us call this "theory" CHESS. All possible positions on a chess-board (plus a flag: "whites to go" or "blacks to go") we shall call propositions of CHESS. The only axiom of CHESS will be the initial position, and the rules of inference - the rules of the game. The rules allow us to pass from one proposition of CHESS to some other ones. Starting with the axiom we get in this way theorems of CHESS. Thus, theorems of CHESS are all possible positions which can be got from the initial position by moving of chess-men according to the rules of the game. Exercise 4.1. Can you provide an unprovable proposition of CHESS? Why is CHESS called formal theory? When somebody offers a "mathematical text" P as a proof of a theorem A in CHESS it means that P is the record of some chess-game stopped in the position A. And we can check its correctness. Here checking is not a serious problem: the rules of the play are formulated precisely enough, and we can write a computer program which will execute the task. Exercise 4.2. Estimate the size of this program in some programming language. Our second example of a formal theory is only a bit more serious. It was proposed by P.Lorenzen, let us call it theory L. Propositions of L are all possible words made of letters a, b, for example: a, aa, aba, abaab. The only axiom of L is the word a, and L has two rules of inference: X X ----- , ----- Xb aXa It means that (in L) from a proposition X we can infer immediately propositions Xb and aXa. For example, proposition aababb is a theorem of L: a |-- ab |-- aaba |-- aabab |-- aababb rule1 rule2 rule1 rule1 This fact is expressed usually as L |-- aababb ( "aababb is provable in L"). Exercise 4.3. a) Describe an algorithm which determines whether a proposition of L is a theorem or not. b) Can you imagine such an algorithm for the theory CHESS? Of course, you can. Thus you see that even having a relatively simple algorithm for proof correctness the problem of provability can appear a very complicated one. A very important property of formal theories is given in the following Exercise 4.4. Show that the set of all theorems of a formal theory is effectively (i.e. recursively) enumerable. It means (theoretically) that for any formal theory a computer program can be written which will print on an (endless) paper tape all theorems of the theory (and nothing else). Unfortunately, such a program cannot solve the problem which the mathematicians are interested in: is a given proposition provable or not. When, sitting near the computer we see our proposition printed, it means that it is provable. But until that moment we cannot know whether the proposition will be printed some time later or it will not be printed at all. T is called a solvable theory (or, effectively solvable) if an algorithm (mechanically applicable computation procedure) is presented for checking whether some proposition is provable using principles of T or not. In the exercise 4.3a you have proved that L is a solvable theory. But in the exercise 4.3b you established that it is hard to state whether CHESS is a "normally solvable" theory or not? Proof correctness checking is always much simpler than provability checking. It can be proved that most mathematical theories are unsolvable, elementary (i.e. first order) arithmetic and set theory included (see, for example, Mendelson [1970]). Mathematical theories normally contain the negation symbol not. In such theories to solve the problem stated in a proposition A means to prove either A or notA. We can try to solve the problem using the enumeration program of the exercise 4.4: let us wait sitting near the computer for until A or notA is printed. If A and notA are printed both, it will mean that T is an inconsistent theory (i.e. one can prove using principles of T some proposition and its negation). But totally we have here 4 possibilities: a) A will be printed, but notA will not (then the problem A has positive solution), b) notA will be printed, but A will not (then the problem A has negative solution), c) A and notA will be printed both (then T is an inconsistent theory), d) neither A nor notA will be printed. In the case d) we will be sitting forever near the computer, but nothing interesting will happen, using principles of T one can neither prove nor disprove the proposition A, and for this reason T is called an incomplete theory. The incompleteness theorem of K.Goedel says that most mathematical theories are incomplete (see Mendelson [1970]). Exercise 4.5. Show that any complete formal theory is solvable. To be continued #4