Hmm. I was thinking that Löb’s Theorem was a theorem in PA, in which case the step going from
PA + ?(?C → C) |- ?(?L → C)
to
PA + ?(?C → C) |- ?(?(?L → C))
seems legitimate given
PA |- (?X → ?(?X))
which we ought to be able to use since PA is part of the theory before the |- symbol.
If we don’t have PA on the left, can we use all the “ingredients” without adding additional assumptions?
In any case, if we do not use the deduction theorem to derive the implication in Löb’s Theorem, what do we use?
Hmm. I was thinking that Löb’s Theorem was a theorem in PA, in which case the step going from
PA + ?(?C → C) |- ?(?L → C)
to
PA + ?(?C → C) |- ?(?(?L → C))
seems legitimate given
PA |- (?X → ?(?X))
which we ought to be able to use since PA is part of the theory before the |- symbol.
If we don’t have PA on the left, can we use all the “ingredients” without adding additional assumptions?
In any case, if we do not use the deduction theorem to derive the implication in Löb’s Theorem, what do we use?