We don’t have PA + X proving anything for any X.
It seems to me that we do have (PA + ”?(◻C → C)” |- ”?C”)
from which the deduction theorem gives: (PA |- ”?(◻C → C) → ?C”) which is Löb’s Theorem itself.
We don’t have PA + X proving anything for any X.
It seems to me that we do have (PA + ”?(◻C → C)” |- ”?C”)
from which the deduction theorem gives: (PA |- ”?(◻C → C) → ?C”) which is Löb’s Theorem itself.