Raymond Smullyan in his book on Gödel's incompleteness theorems introduces a certain axiom system for Peano arithmetic with exponentiation (PE, see below). He then shows that under the assumption that system is correct (i.e., all provable sentences are true for the natural numbers $\mathbf{N}$), one can prove Gödel's first incompleteness theorem.
Now I am wondering if one has to assume that this system is correct, or if one can prove this.
The axioms of PE
and the usual induction axiom
