On Wikipedia it says:
"... the Gödel sentence of Peano arithmetic, is not provable nor disprovable in Peano arithmetic."
When talking about proving something in Peano Arithmetic, are we talking about just using the axioms of Peano Arithmetic (or maybe some model of them), or are we also allowed to use some other logic to make proofs? For example, in the first case, we would not be able to use modus ponens.
So in the first case, we could show that $succ(succ(0))$ is a natural number. But we could not show that $x = 0 \land y = succ(0) \implies y = succ(0)$ because ($\land$) and ($\implies$) just are not symbols of the language of peano arithmetic.