I was thinking that Löb’s Theorem was a theorem in PA
It is a theorem about PA, although everything the statement and the proof of it can be expressed in PA if you like, in which case it is a theorem inside of PA about PA. There’s no contradiction there, as long as you have everything quoted properly.
in which case the step going from
PA + ?(?C → C) |- ?(?L → C)
to
PA + ?(?C → C) |- ?(?(?L → C))
seems legitimate given
PA |- (?X → ?(?X))
That’s a valid deduction, but I don’t think it’s a step that anyone has written down in this thread before. It’s not clear to me where you are going with it.
In any case, if we do not use the deduction theorem to derive the implication in Löb’s Theorem, what do we use?
We use 10 steps, 9 of which are proofs inside of PA, and one of which is the fact that if PA |- X then PA |- “PA |- X”.
simon:
It is a theorem about PA, although everything the statement and the proof of it can be expressed in PA if you like, in which case it is a theorem inside of PA about PA. There’s no contradiction there, as long as you have everything quoted properly.
That’s a valid deduction, but I don’t think it’s a step that anyone has written down in this thread before. It’s not clear to me where you are going with it.
We use 10 steps, 9 of which are proofs inside of PA, and one of which is the fact that if PA |- X then PA |- “PA |- X”.