To argue that a proof is being made concluding ?C using the assumption ?(◻C → C) given the theory PA, to which proof we can apply the deduction theorem to get (PA |- ”?(◻C → C) → ?C”) (i.e. my interpretation of Löb’s Theorem)
We use 10 steps, 9 of which are proofs inside of PA
But the proof uses an additional assumption which is the antecedent of an implication, and comes to a conclusion which is the consequent of the implication. To get the implication, we must use the deduction theorem or something like it, right?
the fact that if PA |- X then PA |- “PA |- X”
Is this fact a theorem of first order logic without any additional assumptions, or is it merely a theorem of PA? I admit I don’t know, as I’m not very familiar with first order logic, but it intuitively seems to me that if first order logic were powerful enough on its own to express concepts like “PA proves X” it would probably be powerful enough to express arithmetic, in which case the qualification in Gödel’s theorem that it only applies to theories that express arithmetic would be superfluous.
It’s not clear to me where you are going with it.
To argue that a proof is being made concluding ?C using the assumption ?(◻C → C) given the theory PA, to which proof we can apply the deduction theorem to get (PA |- ”?(◻C → C) → ?C”) (i.e. my interpretation of Löb’s Theorem)
We use 10 steps, 9 of which are proofs inside of PA
But the proof uses an additional assumption which is the antecedent of an implication, and comes to a conclusion which is the consequent of the implication. To get the implication, we must use the deduction theorem or something like it, right?
the fact that if PA |- X then PA |- “PA |- X”
Is this fact a theorem of first order logic without any additional assumptions, or is it merely a theorem of PA? I admit I don’t know, as I’m not very familiar with first order logic, but it intuitively seems to me that if first order logic were powerful enough on its own to express concepts like “PA proves X” it would probably be powerful enough to express arithmetic, in which case the qualification in Gödel’s theorem that it only applies to theories that express arithmetic would be superfluous.