18
Denoting
Ref(T)
the set of all the sentences refutable in the theory T (i.e. the set of all the
sentences
ϕ such that T |– ¬ϕ), it is obvious that also this set
Ref(T)
is not recursive. Now we
can illustrate mutual relations between the sets
Thm(T)
,
Th(N)
, and
Ref(T)
by the following
figure
22
:
If the (consistent) theory T is recursively axiomatized and complete, the sets
Thm(T),
Th(N)
coincide, and
Ref(T)
is a complement of them.
Another consequence of the Incompleteness theorem is the undecidability of the problem
of logical truth: The FOPL proof calculus is a theory without special axioms. Though it is a
complete calculus (all the logically valid formulas are provable), as an “empty” theory it is
not decidable: there is no algorithm that would
decide any formula
ϕ whether it is a theorem
or not (which equivalently means whether it is a logically valid formula or not). The problem
of logical truth is not decidable in FOPL. For, Q is an adequate theory with a finite number of
axioms. If Q
1
,…Q
7
are its axioms (closed formulas), then a sentence
ϕ is provable in Q iff
(Q
1
& … & Q
7
)
→ ϕ is provable in the FOPL calculus
23
, and so (Q
1
& … & Q
7
)
→ ϕ is a
logically valid formula. If the calculus were decidable so would be Q, which is not.
Alonzo Church proved that the proof calculus is partially decidable: there is an algorithm,
which at an input formula
ϕ that is logically valid outputs the answer Yes. If however the
input formula
ϕ is not a logical truth the algorithm may answer no or it can never output any
answer.
Gödel discovered that the sentence
ν claiming “I am not provable” is equivalent to the
sentence
τ claiming “There is no <ϕ> such that both <ϕ> and <¬ϕ> are in
Thm(T)
”. The
latter is a formal statement that the system is consistent. Since
ν is not provable, and ν and τ
are equivalent,
τ is not provable as well. Thus we have:
Gödel’s Second Theorem on incompleteness. In any consistent recursively axiomatizable
theory T that is strong enough to encode sequences of numbers (and thus the syntactic notions
of “formula”, “sentence”, “proof”) the consistency of the theory T is not provable in T.
The second incompleteness theorem shows that there is no hope of proving, e.g., the
consistency of the first-order arithmetic using finitist means provided we accept that finitist
means are correctly formalized in a theory the consistency of which is provable in PA. As
Georg Kreisel remarked, it would actually provide no interesting information if a theory T
proved its consistency. This is because inconsistent theories prove everything, including their
consistency. Thus a consistency proof of T in T would give us no clue as to whether T really
is consistent.
22
See Švejdar 2002
23
Here we use a Theorem of deduction: Q
1
& … & Q
n
|
− ϕ iff Q
1
& … & Q
n-1
|
− Q
n
→ ϕ
Axioms
Thm(T) Th(N)
Ref(T)
19
One of the first to recognize the revolutionary significance of the incompleteness results
was John von Neumann (Hungarian-born brilliant mathematician) who even almost
anticipated Gödel’s second theorem on incompleteness. Others were slower to absorb the
essence of the problem and to accept its solution. For example, Hilbert’s assistant Paul
Bernays had difficulties with technicalities
24
of the proof that were cleared up only after
repeated correspondence. Gödel’s breakthrough even drew sharp criticism,
which was due to
prevailing conviction that mathematical thinking can be captured by laws of pure symbol
manipulation, and due to inability to make the necessary distinctions involved, such as that
between the notion of truth and proof. Thus, for instance, the famous set-theorist Ernst
Zermelo interpreted the latter in a way that leads to a pure contradiction with Gödel’s results.
3.2. Research after Gödel
Let me close this section by making a remark that Gödel incompleteness theorems,
especially the celebrated 2
nd
Incompleteness Theorem, not only is a brilliant result which
logicians are proud of and which can
be reflected philosophically; it also plays the role of a
useful technical tool for proving theorems about meta-mathematics of axiomatic theories.
Therefore I would like to mention the fact that an interesting research inspired by Gödel
continued also after Gödel
25
.
Since no reasonable axiomatic theory T can prove its own consistency, a theory S capable
of proving the consistency of T can be viewed as considerably stronger than T. Of course,
considerably stronger implies non-equivalent. The Levy Reflection Principle, which is non-
trivial but also not so difficult to prove, says that Zermelo-Fraenkel set theory ZF proves
consistency of each of its finitely axiomatized sub-theories. So by Gödel 2
nd
Incompleteness
Theorem, full ZF is considerably stronger than any of its finitely axiomatized fragments. This
in turn yields a simple proof that ZF is not finitely axiomatizable. The same, with a similar
but a little bit more complicated proof, is true of PA. Also ZF proves the consistency of PA.
As to the research after Gödel, I want to mention the Gentzen consistency proof, Pudlak’s
extensions of Gödel 2
nd
Incompleteness Theorem and the connections of Gödel Theorem to
modal logic.
Gerhard Gentzen, around 1940, raised the following question: once we know that
consistency of Peano arithmetic PA cannot be proved in PA itself but can be proved in ZF,
what exactly of all the set-theoretical machinery is necessary to prove consistency of PA?
Gentzen’s answer was: all we need is to know that the (countable) ordinal
ε
0
,
defined as the
limit or ordinals 1,
ω, ω
ω
, ... is well founded, i.e., it is not a majorant of an infinite decreasing
sequence of ordinals.
Pavel Pudlak in 1980’s showed that Gödel 2
nd
Incompleteness Theorem holds
also for very weak fragments of PA, and if carefully (re)formulated, it holds for the
Robinson’s arithmetic too. He also proved a quantitative version of Gödel 2
nd
Incompleteness
Theorem, saying that statements of the form "there is no proof of contradiction the length of
which is less than n”, while provable in T if T satisfies usual requirements, only have proofs
the lengths of which grow very rapidly with n.
Provability logic is a modal propositional logic where the usual modal operator (Box) is
interpreted as formal provability in some fixed axiomatic theory extending arithmetic. Then
e.g.
¬ False (not provable False) is a modal formula which can be read “contradiction is
unprovable in T”. Its arithmetical counterpart is the formalized consistency statement which,
by Gödel 2nd Incompleteness Theorem, cannot be proved in T. So
¬ False is an example of
24
The technical device used in the proof is now known as Gödel numbering
25
These remarks were formulated by Vítězslav Švejdar. I am deeply grateful for them.