Gödel's theorem

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 A₁,A₂,..A_n 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.