Gödel's second incompleteness theorem can be proven in PA + COH, where PA is Peano Arithmetic and COH the consistency statment. By this I mean : $PA+COH\vdash \neg \square COH$ where $\square P$ means 'P is provable in PA', so that $COH=\neg \square \bot$.
But PA+COH does not prove $\neg \square\neg COH$. However, we know meta-theoratically (in ZFC ?) that COH is undecidable in PA, so PA does not prove $\neg COH$.
So which extra-feature from ZFC are we using that PA+COH does not have in the proof of undecidability of COH ?
The additional assumption is a soundness principle for PA. Perhaps surprisingly, PA does not prove "If I prove $\varphi$, then $\varphi$ is true" for every sentence $\varphi$! In fact, if it does, then it proves $\varphi$ outright - this is Lob's theorem.
A soundness principle is a statement of the form "If PA proves a sentence $\varphi$ of the form [blah], then $\varphi$ is true." Such statements can have lots of strength over PA. In this case, we need soundness for $\Sigma^0_1$ sentences - sentences of the complexity of "there is a proof of...". Goedel originally used a stronger assertion, namely $\omega$-consistency (which, despite the name, is a soundness principle).
However, if we replace "PA is consistent" with the related Rosser sentence $R$, then this discrepancy goes away: PA + "PA is consistent" proves that PA neither proves nor disproves $R$.