Gödel's second incompleteness theorem
Gödels first incompleteness theorem proves that formal
systems T satisfying "certain conditions" are incomplete, i.e. that
there is a sentence A in the language of the T which can neither be
proved, nor disproved in T. Among the "certain conditions" must be
some condition implying that T is consistent.
Gödel's second incompleteness theorem proves that formal
systems T satisfying certain other conditions "cannot prove their own
consistency", in the sense that a suitable formalization in the
language of T of the statement "T is consistent" cannot be proved in
T. Again one necessary condition is that T is in fact consistent,
since otherwise everything is provable in T.
The second incompleteness theorem applies in particular to those
formal systems that can be used to develop all of the ordinary
mathematics that one finds in textbooks. One such system is the axiomatic
set theory called ZFC.
Since all the theorems ordinarily proved in mathematics can be
proved in ZFC, and since the consistency of ZFC cannot be proved in
ZFC (unless ZFC is inconsistent), it is often concluded that we
cannot expect to prove, and therefore can't know, that ZFC is
consistent. "We can't know that mathematics is consistent." This is
the conclusion discussed in this section.
"Different" doesn't mean "stronger"
In commenting on this, first let me mention a widespread
misconception. Clearly, for any theory T, there is another theory T'
in wich "T is consistent" can be proved. For example, we can trivially
define such a theory T' obtained by adding "T is consistent" as a new
axiom to T. The misconception consists in the notion that any such
theory T' in which "T is consistent" is provable must be
stronger than T. This is not true. All that Gödel's second
theorem shows is that T' cannot be the same as T. For
example, the consistency of ZFC can be proved in an extension of
arithmetic obtained by adding "ZFC is consistent" as a new axiom. This
new arithmetical theory is neither stronger, nor weaker than ZFC. The
two theories are logically incomparable. (Although if we remove the
new axiom from the arithmetical theory, we get a theory that is very
much weaker than ZFC.)
There are many consistency proofs
Of course a consistency proof for T in a theory T' obtained by
taking "T is consistent" as an axiom is not very interesting. More
interesting are those consistency proofs obtained by introducing some
other kind of abstract reasoning than that formalized in T. There are
several such consistency proofs for various theories T in the logical
literature, although not for such theories as ZFC.
Consistency proofs for ZFC are essentially proofs by reflection,
meaning that we note, in some way or another, that since the axioms of
ZFC are true, they are consistent. For example, for every finite
subset A1,A2,..An of axioms of ZFC,
it is provable in ZFC that these axioms have a model, hence are
consistent. We can then conclude that ZFC is consistent, since any
inconsistency in ZFC would be an inconsistency in some finite subset
of the axioms of ZFC. (It is probably not obvious why this proof is not
formalizable in ZFC itself, and a technical comment explains the matter further.)
Consistency is a weak condition
Another point which is often overlooked is that consistency is only
a weak soundness property. More precisely, that ZFC is consistent does
not imply that every elementary arithmetical statement provable in ZFC
is true. For example, from a logical point of view there is nothing to
exclude that (i) every even number
greater than 2 is the sum of two primes (Goldbach's conjecture)
even though (ii) it is provable in ZFC that there is an even number
greater than 2 which is not the sum of two primes and (iii) ZFC is
consistent.
For an actual example of a consistent but unsound theory, suppose we
add to ZFC the new axiom "ZFC is inconsistent". If ZFC is consistent,
then the new theory ZFC' is consistent (by Gödel's second theorem),
even though it falsely proves that ZFC is inconsistent.
So is even consistency unknowable?
What then can be said about the conclusion that we can't even know that
mathematics (as formalized in ZFC) is consistent, let alone that it is
sound in some stronger sense? This conclusion is unassailable if we
accept that we can't know that an arithmetical sentence (which the
sentence "ZFC is consistent" becomes when formalized) is true if it
isn't provable in ZFC. There is no obvious reason why we should accept
this. On the contrary, Gödel's theorem can just as well be seen as
showing that we can know the truth of arithmetical sentences not
provable in ZFC, "ZFC is consistent" being an example.
However, even if we reject the view that Gödel's theorem shows that
"we can't know that mathematics is consistent" - and there is nothing
unreasonable about rejecting this view - we must admit that the fact
that "ZFC is consistent" is not provable in ZFC itself means that
there will most likely never be any argument for the consistency of
ZFC that is regarded by a majority of mathematicians as definitive and
unproblematic. This tentative conclusion is based on the fact that ZFC
suffices and more than suffices for formalizing all such unproblematic
reasoning introduced in mathematics so far.