VI
Compared to the axiomatic efforts made at the end
of the nineteenth and
beginning of the twentieth cen-
turies, which
can be regarded retrospectively as naive
or semi-concrete, contemporary
axiomatization is
characterized by three features anticipated, of course,
by what
preceded it, but now sharply asserted and
inseparably united:
symbolization, formalization, and
appeal to meta-theories.
Symbolization consists in substituting for the spoken
natural languages,
with their national differences and
especially their imperfections in
logical respects, a
system of written signs, a
“characteristic,” which is an
immediate ideographic
representation not exactly of
the ideas belonging to the theory
axiomatized, if the
ideas happen to be already represented by signs,
but
of the logical articulations of the discourse in which
the theory
is developed. It is also not yet a question,
therefore, of “the
universal characteristic” dreamed of
by Leibniz, but only of a logical characteristic
which
allows one to express in an entirely artificial symbolism
the
doctrines which, like Arithmetic, already make use
of a symbolism which is
appropriated for their ideas
and operations. Frege in his Begriffsschrift (Halle, 1879)
and Peano in his Notations de logique mathématique
(Turin,
1894) proposed such systems of symbolic logic.
Frege's symbolism was quite
cumbersome and has not
survived, whereas Peano's notation, essentially
what
Russell adopted, has passed into the current usage of
symbolic
logic.
The chief value of this symbolic notation is to make
possible a formal
treatment of the sort of reasoning
about ideas, which is still tainted more
or less with
subjectivity or with appeals to intuition in judging the
correctness of logical inferences, by replacing such
reasoning by a
calculus of signs. Here Leibniz' ideal
of a calculus of reasoning (calculus ratiocinator) comes
to the fore again.
Now in order to avoid any dispute
in the practice of such a calculus, it is
first necessary,
as in a well-regulated game, that the rules governing
the calculus be explicitly formulated, and in such a
manner that they admit
no ambiguity about their mode
of application. That is why formal axiomatic
systems
state the rules according to which calculation may take
place
besides stating the axioms serving as a basis for
the calculus. In that way
the confusion was cleared
up which had prevailed for a long time with
respect
to the distinction, on the level of logical principles,
between premisses and rules of inference. The rules
of inference are now
made explicit and are expressly
distinguished from the system of premisses
on which
the calculus operates governed by the rules. These rules
are
generally divided into two groups, depending on
whether they govern the
formation or the trans-
formation of
expressions. Demonstration then amounts
to transforming progressively,
without omitting any
step, one or more formulas correctly formed (the ab-
breviation “w.f.f.”
is used for “well formed formulas”)
and already
admitted as axioms or theorems, by indi-
cating at each step the number of the rule authorizing
this
transformation, until step by step the formula to
be demonstrated is
finally reached. Such a task has
become performable, in theory and in fact
for rela-
tively simple cases, by a suitably
constructed and
programmed machine; the computing machine can
with
extreme rapidity try the various combinations
authorized by the rules of
inference and retain only
those combinations which yield the result sought.
But how can one be sure, in the unrolling of the
theorems derivable from the
axioms according to these
rules, that one will never run into a
contradiction, that
is to say, into the possibility of proving both a
formula
and the same formula preceded by the sign of negation?
Such a
question was hardly a problem for the first
axiomatic systems which started
from a system of
propositions practically certified, such as the body
of
Euclidean geometry or that of classical arithmetic, and
simply
proposed to make the system rest on a minimal
basis, entirely explicit.
However, the problem of the
consistency of a system arises as soon as there
is a doubt
about it, and furthermore, the problem of consistency
arises also in the reverse direction, when a certain
number of axioms are
arbitrarily posited in order to
see what consequences flow from these
axioms. In order
to be sure that the very axioms of a system are
indeed
compatible, we must rise to a new level and take this
system as
itself an object of study. In his Foundations
of
Geometry of 1899, Hilbert had already raised ques-
tions about his axioms when he investigated their mu-
tual independence, their subdivision into five
groups,
and the limitations which each had to impose on its
own
respective domain. Taking very clearly into con-
sideration the specificity of this class of problems, he
proposed in 1917 the institution of a new science,
“Metamathematics,” which takes as its object of study
the language of mathematics already symbolized and
formalized, and in
abstraction from its meaning pro-
ceeds
entirely on its own in a mathematical manner
to create rigorous proofs. In
this new science the prob-
lem of the proof of
the noncontradictoriness of an
axiomatized mathematical system naturally
occupied
an important place. In truth, however, the difficulty
had
only been pushed back, for it was then necessary
to guarantee the validity
of the metamathematical
procedures themselves. Whence arose the attempts
to
find a means of proving the noncontradictoriness of
a system by
means of the very axioms and rules of
inference within the system itself.
The halting of these attempts and their futility were
explained and
sanctioned by the famous proof by K.
Gödel (1931); the proof
itself was drawn by the rigor-
ous procedures
of metamathematics and established
that the proposition which states the noncontradictori
ness of a system in which arithmetic can be developed
is not
decidable within this system. In other words,
in order to prove that a
formal system is not contra-
dictory, it
is necessary to appeal to stronger means of
demonstration than those used
by the system itself, and
by means of which the question of
noncontradiction
is consequently carried over. Hence the theory about
a calculus cannot be constructed by means of the
resources alone of this
calculus, nor can one speak
about a language without employing a
metalanguage,
which would yield the same uncomfortable situation.
In
short, formalism is not self-sufficient; its closure on
itself is
impossible. The ideal of the calculus ratiocina-
tor and that of the
caracteristica universalis are in the
end
incompatible. One can postpone indefinitely but
cannot eliminate altogether
the appeal to logical
intuitions.
This check on one of the objectives of metamathe-
matics is, in other respects, an important result
to
credit to it. Besides, metamathematical logic poses
many other
problems concerning completeness, decida-
bility, categoricity, isomorphism, etc.; the very analysis
of these
ideas leads to their further diversification by
greater refinements and
nuances. As an example, the
idea of noncontradiction appears as a special
case of
the more general idea of consistency which is itself
presented
in various forms.
Because of the close relationship between logic and
mathematics, which is
highlighted by the formalizing
of their axiomatic systems, logic itself has
experienced
analogous developments. By analogy with Hilbert's
metamathematics, Tarski constructed metalogic as a
distinct discipline.
Beside the questions of syntax which
had at first been the main concern of
metatheories,
Tarski emphasized the importance of the semantic
point
of view. Through this new approach he estab-
lished limiting conditions under which the semantic
notion of truth
replaces the syntactical idea of deriva-
bility; this he showed in a theorem (1935) which, con-
joined to other results, came at the same time in
various
forms to converge on Gödel's result. But here also,
the
field of metatheory was extended to many other prob-
lems. Metalogic today occupies in the activities of
logicians a place equal at least in importance to that
of logic properly
so-called, since beyond the studies
specifically assigned to metalogic
there is scarcely any
work in logic not accompanied by a critical examina-
tion on the metalogical level.
