I have started to learn about Peano Arithmetic, and also about ordinals. In particular, I have seen that the Goodstein theorem is an example of a statement that can be expressed in PA but that requires other axioms to be proven. In particular, ZFC axioms (or just ZF?) let us construct ordinals up to $_0$ and with those we can prove Goodstein theorem.
I have also read that the statement $Cons(PA)$ is expressible in PA itself but cannot be proved in PA (that's Gödel theorem) but that it can be proved with $_0$ induction.
Now my questions are:
- What does it really mean that it can be proved with $_0$ induction? I mean, are there specific axioms we can add to PA to express $_0$ induction or does it just mean that we can prove it in ZFC with the help of $_0$ induction, just like Goodstein's theorem?
- Also, in simple words, what's the idea of such a proof?