> Note that this uses two notions of "true" - provable (can be derived from axioms), and actually true.

Even the second notion of truth actually just semantic consequence of the second-order theory of the naturals, which is a mathematical formal concept, not quite the same as actual (ontological) truth.