Karlis Podnieks (
Fri, 4 Nov 1994 09:09:30 +0200 (EET)

University of Latvia
Institute of Mathematics and Computer Science

K.Podnieks, Dr.Math.


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
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
Presuming that intuitive mathematical concepts can possess some
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
exists independently of mathematical reasoning).
Some of the intuitive concepts admit several different but,
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
sequences of rational numbers. Dedekind defined real numbers as "cuts" in
the set of
rational numbers. One definition more could be obtained using (infinite)
fractions. The equivalence of all these definitions was proved (we cannot
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
reconstructions of this notion were proposed: recursive functions,
of A.M.Turing, lambda-calculus of A.Church, canonical systems of E.Post,
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
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
reconstructions appears in the history of mathematics very definitely.
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
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
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
mathematical platonism, converted into the methodological one (for a
analysis see Podnieks [1981, 1992]).
Does the "axiomatic reasoning" differ in principle from the
mathematical reasoning? Do there exist proofs in mathematics obtained not
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
formalism! Goedel's theorem demonstrates that no fixed fantastic "world
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
many steps of intuitive reasoning, expressed by a specialist very
compactly, appear
very long and tedious in an axiomatic theory. Therefore, after replacing
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
axiomatization allows to "correct" intuition: to remove inaccuracies,
ambiguities and
paradoxes which arise sometimes due to insufficient controllability of
Secondly, axiomatization allows to carry out a detailed analysis
of relations
between basic principles of a theory (to establish its dependence or
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
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?
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
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
(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
(i.e. mechanically applicable computation procedure) is presented for
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
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.
checking is not a serious problem: the rules of the play are formulated
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:
----- , -----
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.
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
(mechanically applicable computation procedure) is presented for checking
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?
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
a) A will be printed, but notA will not (then the problem A has
b) notA will be printed, but A will not (then the problem A has
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

Exercise 4.5. Show that any complete formal theory is solvable.

To be continued #4