This is best understood in terms of models. Prove doesn’t assert that something is provable in our normal sense it asserts that there are numbers encoding a proof. So what “PA |- Prov(phi) → phi” really asserts is that any structure that satisfies the axioms of PA must believe that phi is true iff it believes there is a number coding a proof of phi.
But there are lots of structures other than the usual non-negative integers that satisfy PA. Including ones with infinite ‘numbers.’. In fact, anything consistent with the axioms of PA is going to be true in one of these non-standard models.
So what this is really saying is that if phi isn’t a consequence of PA then there is some structure which contains a fake ‘infinite proof’ of phi but in which phi isn’t true. No paradoxes at all.
This is best understood in terms of models. Prove doesn’t assert that something is provable in our normal sense it asserts that there are numbers encoding a proof. So what “PA |- Prov(phi) → phi” really asserts is that any structure that satisfies the axioms of PA must believe that phi is true iff it believes there is a number coding a proof of phi.
But there are lots of structures other than the usual non-negative integers that satisfy PA. Including ones with infinite ‘numbers.’. In fact, anything consistent with the axioms of PA is going to be true in one of these non-standard models.
So what this is really saying is that if phi isn’t a consequence of PA then there is some structure which contains a fake ‘infinite proof’ of phi but in which phi isn’t true. No paradoxes at all.