Why is Gödel's Second Incompleteness Theorem important?
Given that the consistency of a system can be proven outside of the given formal system, Gödel says,
It must be noted that proposition XI... represents no contradiction to the formalities viewpoint of Hilbert....
Why do others disagree?
Who cares whether a system cannot prove its own consistency? Why would we expect such a thing?
Is it possible that a theory without multiplication, but with some other axiom or axioms (i.e., weaker in one sense but stronger in another) could prove P consistent and itself consistent?
Solution 1:
You asked in a comment:
Who cares if a theory can prove itself consistent, if it can be proven using some other method?
Let us first observe that inconsistent theories are entirely worthless. You want to know if $X$ is true, and then you prove that it is a consequence of theory $T$, so you now go around believing $X$. If you later find that $T$ is inconsistent, then $T$ cannot lend any support whatever to $X$. You might as well be flipping coins to decide what theorems are true. $T$ is worthless; you will have to find some other reason to believe $X$.
So you would like to find some theory $T$ for which you have good reason to believe $T$ is consistent. One plausible-seeming method is to choose axioms that are as simple as possible and which seem intuitively true. But the crisis of set theory around 1905 shows that this method does not always work. The comprehension axiom of naïve set theory is as simple and intuitively plausible as anything, and it is false. The discovery that it was false precipitated the formalist programs of Hilbert and Whitehead & Russell, and was the direct motivation for Gödel's work.
So you might like a proof that theory $T$ is consistent. Unfortunately, Gödel's theorem shows that $T$ cannot do it and neither can any theory strictly weaker than $T$. So if you want to show that $T$ is not completely worthless, you need a theory, say $T'$, that is stronger in at least one aspect. So suppose you show that $T$ is consistent, using $T'$.
If $T'$ is chosen to be strictly stronger than $T$, so that $T'$ shows as much as $T$ does and also shows that $T$ is consistent, then now you are in a very stupid position. If you weren't sure that $T$ was consistent, $T'$ cannot help you, because if $T$ is inconsistent, then so is $T'$. So you didn't trust $T$, but you have even less reason to trust $T'$. Suppose Shady Joe offers to sell you the Empire State Building for $5. You are not sure, and suspect that Joe is trying to scam you. Joe insists that he is honest, and suggests his Uncle Louie as a character witness. So you go up to the state prison where Uncle Louie is serving a fifteen-year sentence for fraud, and, from his prison cell, Louie assures you that Shady Joe is offering you a fair deal.
But this is exactly the position we are in. We would like to prove things about numbers, say the twin prime conjecture. We have the Peano axioms, which we believe capture how numbers work. But how do we know that from these axioms there is not some proof, perhaps a very long one, that $4923 = 4925$? This would not show that $4923$ actually equals $4925$; it would only show that PA was broken. We would have to throw away PA and use something else instead, as we did with naïve set theory. If we knew that PA was consistent, we would know that there was no such proof. And there is a proof of the consistency of PA using ZF set theory! But this is like asking Uncle Louie if Shady Joe is telling the truth, because if PA is inconsistent, then so is ZFC; if PA was inconsistent, then ZFC would prove that PA was consistent anyway.
Solution 2:
Hilbert's program aimed at "solving" the foundational issues (form Cantor and Frege, to Russell and Brouwer) proving the consistency of the "main" mathematical theories, like arithmetic, real analysis and set theory.
In order to prove that, the program developed concepts and tools of metamathematics, i.e. the discipline based on mathematical logic able to study the mathematical theories as mathematical objcets themselves.
This metamathematical activity has to be "performed" into a "secure" mathematical theory: the "elementary" part of arithmetic.
This theory must supply the tools sufficient for the consistency proof of other theories.
Of course, this "gound-level" mathematical theory must be itself consistent.
Unfortunately, Gödel's Second Incompleteness Theorem shows that a formalized arithmetical theory having "enough resources" (this concept is made precise by the theorem) to be suitable for the metamatheatical aims is not able to prove its own consistency, and neither the consistency of "more powerful" theories like real analysis and set theory.
Regarding Gödel's comment after Th.XI :
I wish to note expressily that Theorem XI do not contradict Hilbert's formalistic viewpoint [emphasis added]. For this viewpoint presupposes only the existence of a consistency proof in which nothing but finitary means of proof is used, and it is conceivable that there exist finitary proofs that cannot be expressed in the formalism of $P$.
And this was exactly what happened with Gentzen's consistency proof.
Some comments are useful here :
-
Hilbert's concept of finitary is not precise: but it's hard to escape from the expectation that the "finitary part" of arithmetic must include $\mathsf{PA}$; thus, G's Th applies.
-
Gentzen's proof is hardly "finitistic".
-
the original aim of Hilbert's program was to "convince" intuitionstic mathematicians that axiomatized set theory was "secure"; if so, any "ostensive" consistency proof based on a model of, e.g. arithmetic, built up into set theory was clearly useless.
Added
Regarding your added question, you can see (in general) :
- Peter Smith, An Introduction to Gödel's Theorems (2nd ed 2013).
In particular, you can see the overview of Presburger's arithmetic for a (very weak) first-order theory of the natural numbers with addition, without multiplication.
This theory is complete and decidable; thus, it "eludes" G's First Th.
Unfortunately, without multiplication it has not enough resources to implement the arithmetization of syntax; thus, it is unable to "perform" the basic metamathematical tasks and so it cannot prove relevant metamathemetical properties, like consistency of a theory (and neither of itself).
Gentzen's consistency proof "eludes" in some way G's Second Th :
Gentzen showed that the consistency of first-order arithmetic is provable, over the base theory of primitive recursive arithmetic with the additional principle of quantifier-free transfinite induction up to the ordinal $ε_0$.
Gentzen's proof also highlights one commonly missed aspect of Gödel's second incompleteness theorem. It is sometimes claimed that the consistency of a theory can only be proved in a stronger theory. The theory obtained by adding quantifier-free transfinite induction to primitive recursive arithmetic proves the consistency of first-order arithmetic but is not stronger than first-order arithmetic.
For example, it does not prove ordinary mathematical induction for all formulae, while first-order arithmetic does (it has this as an axiom schema). The resulting theory is not weaker than first-order arithmetic either, since it can prove a number-theoretical fact - the consistency of first-order arithmetic - that first-order arithmetic cannot. The two theories are simply incomparable.