Delivery-Date:
Date: Fri, 4 Nov 1994 09:09:30 +0200 (EET)
From: Karlis Podnieks <podnieks@mii.lu.lv>
To: QED discussions <qed@mcs.anl.gov>
Subject: Semantics
Message-Id: <Pine.SUN.3.91.941104090541.17702A-100000@sisenis.mii.lu.lv>
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