7
connectives (
¬, &, ∨, →, etc.), quantifiers (∀, ∃) and = (identity)
are not interpreted, they
have the fixed standard meaning
10
.
Some formulas are true under every interpretation for any valuation of variables, i.e., they
are valid in any interpretation structure. They are called logically valid formulas (also logical
truths or
logical laws)
. For instance, the formula [
∀x P(x) ∨ ∀x Q(x)] → ∀x [P(x) ∨ Q(x)] is a
logical truth. Indeed, if the antecedent [
∀x P(x) ∨ ∀x Q(x)] of the implication is true under
some interpretation over a universe U, then either the realization P
U
of the symbol ‘P’ is equal
to U or the realization Q
U
of ‘Q’ is equal to U, or both. Which means that the set-theoretical
union of the sets P
U
and Q
U
is equal to U (P
U
∪ Q
U
= U), and the consequent
∀x [P(x) ∨ Q(x)]
is true under this interpretation as well. According to the definition of implication the whole
formula is true; it cannot be false under any interpretation.
Summarizing: By
M
|
= ϕ[e] we denote the fact that a formula ϕ is satisfied by the
structure
M
and a valuation e. In other words, the formula
ϕ is true under the interpretation
over
M
, for the valuation e. If
ϕ is true under
M
for all valuations e (of variables by elements
of the universe), then
M
is a model of
ϕ, or ϕ is
valid in
M
; in symbols
M
|
= ϕ. Formula ϕ is
logically valid (logical truth), if
ϕ is true under every interpretation, denoted |= ϕ.
2.2. Hilbert’s program
Before introducing Gödel’s results I have to briefly describe the atmosphere in which they
appeared. Paradoxes and conceptual problems of mathematics often stem from the infinite.
This includes, for example, Zeno’s paradoxes in Greek times, infinitesimals in the
seventeenth century, and the paradoxes of set theory in the late nineteenth and early twentieth
centuries. In any case, the problem appeared when mathematicians began to reason with
infinite quantities.
The German mathematician David Hilbert (1862-1943) announced his program in the
early 1920s. It calls for a formalization of all of mathematics in axiomatic form, and of
proving the consistency of such formal axiom systems. The consistency proof itself was to
be carried out using only what Hilbert called “finitary” methods. The special epistemological
character of finitary reasoning then yields the required justification of classical mathematics.
Although Hilbert proposed his program in this form only in 1921, it can be traced back until
around 1900, when he first pointed out the necessity of giving a direct consistency proof of
analysis. Hilbert first thought that the problem had essentially been solved by Russell’s type
theory in Principia. Nevertheless, other fundamental problems of axiomatics remained
unsolved, including the problem of the “decidability of every mathematical question”, which
also traces back to Hilbert’s 1900 address.
Within the next few years, however, Hilbert came to reject Russell’s logicistic solution to
the consistency problem for arithmetic. In three talks in Hamburg in the summer of 1921
Hilbert presented his own proposal for a solution to the problem of the foundation of
mathematics. This proposal incorporated Hilbert’s ideas from 1904 regarding direct
consistency proofs, his conception of axiomatic systems, and also the technical developments
in the axiomatization of mathematics in the work of Russell as well as the further
developments carried out by him and his collaborators. What was new was the finitary way in
which Hilbert wanted to carry out his consistency project.
He accepted Kant’s finitist view in the sense that we obviously cannot experience
infinitely many events or move about infinitely far in space. However, there is no upper
bound on the number of steps we execute. No matter how many steps we may have executed,
10
For details and precise definitions see, e.g., Mendelson (1997)
8
we can always move a step further. But at any point we will have acquired only a finite
amount of experience and have taken only a finite number of steps. Thus, for a Kantian like
Hilbert, the only legitimate infinity is a potential infinity, not the actual infinity. The Kantian
element of Hilbert’s view is what separates his formalism from earlier, implausible accounts.
Hilbert’s problem, as he saw it, lies in how infinite mathematics can be incorporated into the
finite Kantian framework. Hilbert would say that finitist mathematical truths, intimately
bound up with our perception, could be known a priori, with complete certainty. If we were
content with finitist mathematics, this would be the end of the story. But Hilbert wanted more
than this, and rightly so. He wanted to keep the extraordinary beauty, power and utility of
classical mathematics, but he also wanted to do it in such a way that we could be fully
confident that no more paradoxes would arise. This includes transfinite set theory, about
which he declared: “No one shall drive us out of the paradise that Cantor has created for us”.
11
What Hilbert needs to do is to show that various parts of infinite mathematics will fit with
one another and finite mathematics in such a way that no inconsistency could be derived. But
what is involved in deriving things, in mathematical reasoning? Hilbert fixes on the symbols
themselves. Here is the core of formalism: mathematics is about symbols. Hilbert’s Kantian
idea is now to study these symbols mathematically, not using the questionable infinity, but
rather finite meaningful mathematics intimately linked to concrete symbols of classical
mathematics itself. Hilbert was convinced that mathematical thinking could be captured by
the syntactic laws of pure symbol manipulation
12
.
Work on the program progressed significantly in the 1920s and many outstanding
logicians and mathematicians took part in it, such as Paul Bernays, Wilhelm Ackermann, John
von Neumann, Jacques Herbrand and, of course, Kurt Gödel.
2.3. Completeness of the proof calculus
The idea of finitist axiomatisation is simple: if we choose some basic formulas (axioms)
that are decidedly true and if we use a finite method of applying some simple rules of
inference that preserve truth, no falsehood can be derived from these axioms; hence no
contradiction can be derived, no paradox can arise.
Logically valid formulas that are true under each interpretation are the most indisputably
true formulas. Let us consider some logically valid formulas:
(1)
ϕ → (ψ → ϕ)
(2)
(
ϕ → (ψ → ξ)) → ((ϕ → ψ) → (ϕ → ξ))
(3)
(
¬ϕ → ¬ψ) → (ψ → ϕ)
(4)
∀x ϕ(x) → ϕ(c) (where
c is a constant or a suitable
variable,
ϕ(c)
arises from
ϕ(
x) by correct substituting
c for
x)
(5)
∀x (ϕ → ψ(x)) → (ϕ → ∀x ψ(x)) (variable x does not occur free in the formula ϕ)
We can easily see that (1)–(5) are logically valid. For instance, (1) says that if
ϕ is true
then it is implied by any
ψ, which is true due to the definition of mathematical notion of
implication. The exact verification is however out of scope of the present article.
11
Brown (1999), Hilbert (1926, p.170): “Aus dem Paradies, daß Cantor uns geschaffen, soll uns niemand
vertreiben können“.
12
In advance we can state at this point that Gödel’s Incompleteness results showed that this belief in the power
of symbol manipulation was not realistic. Actually, Gödel’s results delimitate the possibilities of mechanical
symbol manipulation.