How to prove a non-provable statement? That is weird...
Solution 1:
The statements of Gödel's theorems are about (for simplicity) a certain formal theory, namely $PA$, known as Peano's arithmetic (actually they're more general but I'll stick to that). This theory contains axioms, such as $\forall x \forall y, x\times s(y) = x\times y + x$ and many others.
Now there is also a formal system that allows one to deduce theorems from these axioms; one such theorem would be $\forall x \forall y, x\times y = y\times x$.
There are also sentences $\phi$ that can be expressed in this language that cannot be proved or refuted in this theory. This is somewhat to be expected, indeed if I have no axioms for instance, then clearly I can't prove much beyond logical tautologies (although it's not so easy to see what one can prove without axioms, but that's another question), so we can expect that with too few axioms, some things are left undecided (why should we have found all the right axioms ?)
However we also have a "model" for these axioms, that is in a sense a universe in which these are true. Such a "universe" is $\mathbb{N}$. In this universe all axioms in $PA$ are true, and therefore all theorems of $PA$ are true as well. However, a statement $\phi$ that cannot be proved or refuted in $PA$ has a truth value in $\mathbb{N}$ : it is either true or false (which is not to be mistaken with "either provable or refutable"). The sentences that are true in $\mathbb{N}$ are sometimes called statements of "true arithmetic".
Since we work in a much more powerful theory than $PA$ (namely ZF) we can prove things about $\mathbb{N}$ that go beyond the theorems of $PA$. Obviously what we prove can't contradict the theorems of $PA$, but we can prove things that $PA$ can't. In particular it is not surprising that we can decide sentences that $PA$ can't: Gödel's first incompleteness theorem says that this is the case; there is a statement $\phi$ that is part of true arithmetic (it is true in $\mathbb{N}$, and for vulgarization purposes one may say it is true) but it is not provable from $PA$. In short, there are true but unprovable sentences.
Now if you add to Peano all statements of true arithmetic you obtain... true arithmetic ! Since the Peano axioms are true in $\mathbb{N}$, they are part of true arithmetic, so true arithmetic + $PA$ = true arithmetic. However, as each sentence is either true or false in $\mathbb{N}$, it means that this new theory (sometimes written $Th(\mathbb{N})$ for "theory of $\mathbb{N}$") decides every statement: every statement is provable or refutable from this, so there will be no more "true but unprovable statements".
This seems to contradict Gödel's theorem, but actually it doesn't since $Th(\mathbb{N})$ doesn't satisfy the hypotheses of this theorem, indeed it is not recursively axiomatizable, which means there is no algorithm that can decide whether a given sentence $\phi$ is an axiom. So it's a pretty "lousy" theory in the sense that we can't use it, contrary to $PA$. Gödel's theorem doesn't say that any theory about the integers has true but unprovable statements, it says that any such usable theory has true but unprovable statements.
Hope this makes things clearer
Solution 2:
Intuitively: consider the statement
''this statement is not provable in the theory $T$''.
This statement is true if it is not provable in $T$.
Godel has formally proved that such a statement can be expressed, and it and its negation are not provable, in any theory that contains Peano arithmetics.
And adding the statement as a new axiom gives a new theory in wich we can define a new not provable statement of the same kind.
Solution 3:
There are two points here:
-
In the context of arithmetic, the term "true" means "true in the structure $\Bbb N$. So when Gödel's theorem states that there is a "true statement which is not provable", it means "true in the natural numbers" and not provable from $\sf PA$, or whatever relevant axiomatic system we're talking about.
But truth, even in the natural numbers, might depend on your meta-theory. This is a fickle question, since the choice of meta-theory depends a lot on the mathematician. But I guess most people would agree that since $\sf PA$ is consistent, the statement "$\sf PA$ is consistent" (which can be formulated as the non-existence of a solution for a Diophantine equation, for concreteness) is true, but it is not provable.
-
The incompleteness theorem does not state "every sufficiently complicated system is incomplete". Rather it states that "every sufficiently complicated system which can be recognized by a computer is incomplete". If we add all the true statements, then we get a complete theory, but this theory is no longer recognizable by a computer. Namely, we cannot write an algorithm to tell us whether a certain statement is an axiom of our theory or not.
This is bad, because the fact we can use a computer to verify our axioms means that we can use a computer to verify our proofs. And so the incompleteness theorem tells us that if we want to forego the incompleteness, we can no longer use machinated proof verification. And since humans tends to make mistakes, well, that's not ideal.
In any case, you prove things with a stronger theory. The statement $x\cdot y=y\cdot x$ is not provable from just the axioms of the group. After all, not every group is Abelian. But you can prove this once you add it as an axiom, or add a stronger axiom like $x\cdot x=1$.
Solution 4:
For each sentence $\phi$ in the Peano's arithmetic you have $\mathbb{N}\models\phi$ or $\mathbb{N}\models\neg\phi$ but not both, i.e. you have that $\phi$ or $\neg\phi$ is true in $\mathbb{N}$.
Gödel's second incompleteness theorem says that there exists a sentence $\phi$ such that neither $\phi$ nor $\neg\phi$ is provable in Peano's arithmetic. However one of them is true (in the structure $\mathbb N$).